--- a/IMP/Equiv.ML Fri Dec 02 16:13:34 1994 +0100
+++ b/IMP/Equiv.ML Wed Dec 07 14:11:22 1994 +0100
@@ -11,15 +11,10 @@
addSEs evala_elim_cases)));
val aexp_iff = store_thm("aexp_iff", result() RS spec);
-
-goal HOL.thy "(? x. x=t & P) = P";
-by(fast_tac HOL_cs 1);
-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))));
+ addsimps (aexp_iff::B_simps@evalb_simps))));
val bexp_iff = store_thm("bexp_iff", result() RS spec);
val bexp1 = bexp_iff RS iffD1;