More fixes for HOL changes to Inductive syntax

CakeML · Nov 8, 2023 · 24f0fa5 · 24f0fa5
1 parent aeb8c0f
commit 24f0fa5
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 19 deletions.
diff --git a/candle/prover/permsScript.sml b/candle/prover/permsScript.sml
@@ -87,44 +87,44 @@ Inductive perms_ok:
 [~Conv:]
   (∀ps opt vs.
      EVERY (perms_ok ps) vs ⇒
-       perms_ok ps (Conv opt vs)) ∧
+       perms_ok ps (Conv opt vs))
 [~Closure:]
   (∀ps env n x.
      perms_ok_env ps (freevars x DIFF {Short n}) env ∧
      perms_ok_exp ps x ⇒
-       perms_ok ps (Closure env n x)) ∧
+       perms_ok ps (Closure env n x))
 [~Recclosure:]
   (∀ps env f n.
      perms_ok_env ps
                   (BIGUNION (set (MAP (λ(fn,vn,x). freevars x DIFF
                                                    {Short fn; Short vn}) f)))
                   env ∧
      EVERY (perms_ok_exp ps) (MAP (SND o SND) f) ⇒
-       perms_ok ps (Recclosure env f n)) ∧
+       perms_ok ps (Recclosure env f n))
 [~Vectorv:]
   (∀ps vs.
      EVERY (perms_ok ps) vs ⇒
-       perms_ok ps (Vectorv vs)) ∧
+       perms_ok ps (Vectorv vs))
 [~Litv:]
   (∀ps lit.
-     perms_ok ps (Litv lit)) ∧
+     perms_ok ps (Litv lit))
 [~FP_WordTree:]
   (∀ fp.
-     perms_ok ps (FP_WordTree fp)) ∧
+     perms_ok ps (FP_WordTree fp))
 [~FP_BoolTree:]
   (∀ fp.
-     perms_ok ps (FP_BoolTree fp)) ∧
+     perms_ok ps (FP_BoolTree fp))
 [~Real:]
   (∀ r.
-     perms_ok ps (Real r)) ∧
+     perms_ok ps (Real r))
 [~Loc:]
   (∀ps loc.
      RefMention loc ∈ ps ⇒
-       perms_ok ps (Loc loc)) ∧
+       perms_ok ps (Loc loc))
 [~Env:]
   (∀ps env ns.
      perms_ok_env ps UNIV env  ⇒
-       perms_ok ps (Env env ns)) ∧
+       perms_ok ps (Env env ns))
 [~env:]
   (∀ps fvs env.
      (∀n v.

diff --git a/candle/standard/syntax/holSyntaxScript.sml b/candle/standard/syntax/holSyntaxScript.sml
@@ -462,48 +462,48 @@ Inductive proves:
 [~ABS:]
   (¬(EXISTS (VFREE_IN (Var x ty)) h) ∧ type_ok (tysof thy) ty ∧
    (thy, h) |- l === r
-   ⇒ (thy, h) |- (Abs (Var x ty) l) === (Abs (Var x ty) r)) ∧
+   ⇒ (thy, h) |- (Abs (Var x ty) l) === (Abs (Var x ty) r))
 
 [~ASSUME:]
   (theory_ok thy ∧ p has_type Bool ∧ term_ok (sigof thy) p
-   ⇒ (thy, [p]) |- p) ∧
+   ⇒ (thy, [p]) |- p)
 
 [~BETA:]
   (theory_ok thy ∧ type_ok (tysof thy) ty ∧ term_ok (sigof thy) t
-   ⇒ (thy, []) |- Comb (Abs (Var x ty) t) (Var x ty) === t) ∧
+   ⇒ (thy, []) |- Comb (Abs (Var x ty) t) (Var x ty) === t)
 
 [~DEDUCT_ANTISYM:]
   ((thy, h1) |- c1 ∧
    (thy, h2) |- c2
    ⇒ (thy, term_union (term_remove c2 h1)
                       (term_remove c1 h2))
-           |- c1 === c2) ∧
+           |- c1 === c2)
 
 [~EQ_MP:]
   ((thy, h1) |- p === q ∧
    (thy, h2) |- p' ∧ ACONV p p'
-   ⇒ (thy, term_union h1 h2) |- q) ∧
+   ⇒ (thy, term_union h1 h2) |- q)
 
 [~INST:]
   ((∀s s'. MEM (s',s) ilist ⇒
              ∃x ty. (s = Var x ty) ∧ s' has_type ty ∧ term_ok (sigof thy) s') ∧
    (thy, h) |- c
-   ⇒ (thy, term_image (VSUBST ilist) h) |- VSUBST ilist c) ∧
+   ⇒ (thy, term_image (VSUBST ilist) h) |- VSUBST ilist c)
 
 [~INST_TYPE:]
   ((EVERY (type_ok (tysof thy)) (MAP FST tyin)) ∧
    (thy, h) |- c
-   ⇒ (thy, term_image (INST tyin) h) |- INST tyin c) ∧
+   ⇒ (thy, term_image (INST tyin) h) |- INST tyin c)
 
 [~MK_COMB:]
   ((thy, h1) |- l1 === r1 ∧
    (thy, h2) |- l2 === r2 ∧
    welltyped(Comb l1 l2)
-   ⇒ (thy, term_union h1 h2) |- Comb l1 l2 === Comb r1 r2) ∧
+   ⇒ (thy, term_union h1 h2) |- Comb l1 l2 === Comb r1 r2)
 
 [~REFL:]
   (theory_ok thy ∧ term_ok (sigof thy) t
-   ⇒ (thy, []) |- t === t) ∧
+   ⇒ (thy, []) |- t === t)
 
 [~axioms:]
   (theory_ok thy ∧ c ∈ (axsof thy)