IMP/Equiv.ML

 goal Equiv.thy "!n. (<a,s> -a-> n) = (n = A(a,s))";
 by (aexp.induct_tac "a" 1);                		  (* struct. ind. *)
 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;
 
 val BfstI = read_instantiate_sg (sign_of Equiv.thy)

 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);
 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);
 
 goal Equiv.thy "!io:C(c). <c,fst(io)> -c-> snd(io)";

 by (rewrite_goals_tac [Gamma_def]);  
 by (safe_tac comp_cs);
 by (EVERY1 [dtac bspec, atac]);
 by (ALLGOALS (asm_full_simp_tac com_ss));
 
-val com2 = result();
+qed "com2";
 
 
 (**** Proof of Equivalence ****)
 
 val com_iff_cs = set_cs addEs [com2 RS bspec] addDs [com1];

 (* => *)
 by (fast_tac com_iff_cs 1);
 (* <= *)
 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";