IMP/Equiv.ML

--- a/IMP/Equiv.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/IMP/Equiv.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -9,18 +9,18 @@
 by (ALLGOALS(simp_tac (HOL_ss addsimps A_simps)));	  (* rewr. Den.   *)
 by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems)
                              addSEs evala_elim_cases)));
-val aexp_iff = result() RS spec;
+val aexp_iff = store_thm("aexp_iff", result() RS spec);
 
 
 goal HOL.thy "(? x. x=t & P) = P";
 by(fast_tac HOL_cs 1);
-val elim_ex_conv = result();
+qed "elim_ex_conv";
 
 goal Equiv.thy "!w. (<b,s> -b-> w) = (w = B(b,s))";
 by (bexp.induct_tac "b" 1);
 by (ALLGOALS(asm_simp_tac (HOL_ss addcongs [conj_cong]
               addsimps (aexp_iff::elim_ex_conv::B_simps@evalb_simps))));
-val bexp_iff = result() RS spec;
+val bexp_iff = store_thm("bexp_iff", result() RS spec);
 
 val bexp1 = bexp_iff RS iffD1;
 val bexp2 = bexp_iff RS iffD2;
@@ -51,7 +51,7 @@
 by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
 by (fast_tac (comp_cs addSIs [bexp1,BfstI] addSDs [BfstD,bexp1]) 1);
 
-val com1 = result();
+qed "com1";
 
 
 val com_ss = prod_ss addsimps (aexp_iff::bexp_iff::evalc.intrs);
@@ -73,7 +73,7 @@
 by (EVERY1 [dtac bspec, atac]);
 by (ALLGOALS (asm_full_simp_tac com_ss));
 
-val com2 = result();
+qed "com2";
 
 
 (**** Proof of Equivalence ****)
@@ -87,4 +87,4 @@
 (* <= *)
 by (REPEAT (step_tac com_iff_cs 1));
 by (asm_full_simp_tac (prod_ss addsimps [surjective_pairing RS sym])1);
-val com_equivalence = result();
+qed "com_equivalence";