Manual changes

Author: dnezam

src/1/ConseqConvScript.sml

@@ -62,11 +62,11 @@ Ho_Rewrite.REWRITE_TAC [FORALL_BOOL]);
 val OR_CLAUSES_THML =
      (CONJUNCTS (Ho_Rewrite.PURE_REWRITE_RULE [FORALL_AND_THM] OR_CLAUSES))
 
-Theorem OR_CLAUSES_TX = el 1 OR_CLAUSES_THML
-Theorem OR_CLAUSES_XT = el 2 OR_CLAUSES_THML
-Theorem OR_CLAUSES_FX = el 3 OR_CLAUSES_THML
-Theorem OR_CLAUSES_XF = el 4 OR_CLAUSES_THML
-Theorem OR_CLAUSES_XX = el 5 OR_CLAUSES_THML
+val OR_CLAUSES_TX = save_thm ("OR_CLAUSES_TX", el 1 OR_CLAUSES_THML)
+val OR_CLAUSES_XT = save_thm ("OR_CLAUSES_XT", el 2 OR_CLAUSES_THML)
+val OR_CLAUSES_FX = save_thm ("OR_CLAUSES_FX", el 3 OR_CLAUSES_THML)
+val OR_CLAUSES_XF = save_thm ("OR_CLAUSES_XF", el 4 OR_CLAUSES_THML)
+val OR_CLAUSES_XX = save_thm ("OR_CLAUSES_XX", el 5 OR_CLAUSES_THML)
 
 
 
@@ -100,11 +100,11 @@ val IMP_CONG_simple_imp_weaken = store_thm ("IMP_CONG_simple_imp_weaken",
 val IMP_CLAUSES_THML =
      (CONJUNCTS (Ho_Rewrite.PURE_REWRITE_RULE [FORALL_AND_THM] IMP_CLAUSES))
 
-Theorem IMP_CLAUSES_TX = el 1 IMP_CLAUSES_THML
-Theorem IMP_CLAUSES_XT = el 2 IMP_CLAUSES_THML
-Theorem IMP_CLAUSES_FX = el 3 IMP_CLAUSES_THML
-Theorem IMP_CLAUSES_XX = el 4 IMP_CLAUSES_THML
-Theorem IMP_CLAUSES_XF = el 5 IMP_CLAUSES_THML
+val IMP_CLAUSES_TX = save_thm ("IMP_CLAUSES_TX", el 1 IMP_CLAUSES_THML)
+val IMP_CLAUSES_XT = save_thm ("IMP_CLAUSES_XT", el 2 IMP_CLAUSES_THML)
+val IMP_CLAUSES_FX = save_thm ("IMP_CLAUSES_FX", el 3 IMP_CLAUSES_THML)
+val IMP_CLAUSES_XX = save_thm ("IMP_CLAUSES_XX", el 4 IMP_CLAUSES_THML)
+val IMP_CLAUSES_XF = save_thm ("IMP_CLAUSES_XF", el 5 IMP_CLAUSES_THML)
 
 
 
@@ -126,9 +126,9 @@ val COND_CLAUSES_THML =
      (CONJUNCTS (Ho_Rewrite.PURE_REWRITE_RULE [FORALL_AND_THM] COND_CLAUSES))
 fun bool_save_thm (s,t) = store_thm (s, t, Ho_Rewrite.REWRITE_TAC [FORALL_BOOL])
 
-Theorem COND_CLAUSES_CT = el 1 COND_CLAUSES_THML
-Theorem COND_CLAUSES_CF = el 2 COND_CLAUSES_THML
-Theorem COND_CLAUSES_ID = COND_ID
+val COND_CLAUSES_CT = save_thm ("COND_CLAUSES_CT", el 1 COND_CLAUSES_THML)
+val COND_CLAUSES_CF = save_thm ("COND_CLAUSES_CF", el 2 COND_CLAUSES_THML)
+val COND_CLAUSES_ID = save_thm ("COND_CLAUSES_ID", COND_ID)
 val COND_CLAUSES_TT = bool_save_thm ("COND_CLAUSES_TT",
        ``!c x. (if c then T else x) = (~c ==> x)``)
 val COND_CLAUSES_FT = bool_save_thm ("COND_CLAUSES_FT",

src/1/theory_tests/addMLdep1Script.sml

@@ -4,6 +4,6 @@ Libs
 
 val _ = add_ML_dependency "MLdepLib"
 
-Theorem thm = TRUTH;
+val thm = save_thm("thm", TRUTH);
 
 

src/1/theory_tests/addMLdep2Script.sml

@@ -18,4 +18,4 @@ fun grep s fname =
 val _ = if grep "MLdepLib" "addMLdep1Theory.sml" then ()
         else OS.Process.exit OS.Process.failure
 
-Theorem thm2 = TRUTH;
+val _ = save_thm("thm2", TRUTH);

src/1/theory_tests/gh225aScript.sml

@@ -2,7 +2,7 @@ Theory gh225a[bare]
 Libs
   HolKernel Parse boolLib
 
-Theorem Empty = TRUTH;
-Theorem GREATER = TRUTH;
+val _ = save_thm("Empty", TRUTH);
+val _ = save_thm("GREATER", TRUTH);
 
 

src/1/theory_tests/gh225bScript.sml

@@ -4,5 +4,5 @@ Ancestors
 Libs
   HolKernel Parse boolLib
 
-Theorem TRUTH = TRUTH;
+val _ = save_thm("TRUTH", TRUTH);
 

src/1/theory_tests/gh403aScript.sml

@@ -2,5 +2,5 @@ Theory gh403a[bare]
 Libs
   HolKernel boolLib
 
-Theorem print = TRUTH;
+val _ = save_thm("print",TRUTH);
 

src/1/theory_tests/gh403bScript.sml

@@ -4,5 +4,5 @@ Ancestors
 Libs
   HolKernel boolLib
 
-Theorem foo = TRUTH
+val _ = save_thm("foo", TRUTH)
 

src/1/theory_tests/github115aScript.sml

@@ -15,5 +15,5 @@ val _ = assert
                    HOLset.member(atoms, v2))
           t
 
-Theorem th = DISCH_ALL (ASSUME t)
+val th = save_thm("th", DISCH_ALL (ASSUME t))
 

src/1/theory_tests/github115bScript.sml

@@ -10,5 +10,5 @@ Libs
    corrupt Theory.sml file)
 *)
 
-Theorem sample2 = AND_CLAUSES
+val sample2 = save_thm("sample2", AND_CLAUSES)
 

src/1/theory_tests/github130bScript.sml

@@ -4,6 +4,6 @@ Ancestors
 Libs
   HolKernel Parse boolLib github130Lib
 
-Theorem gh130b = boolTheory.AND_CLAUSES;
+val _ = save_thm("gh130b", boolTheory.AND_CLAUSES);