# HG changeset patch # User nipkow # Date 786805882 -3600 # Node ID 2757544bbe6ddb54a8e31fd3999d83ced96cfadf # Parent 61620d959717ecb4b9aa5c5664e22d739361bc5d Removed a local lemma which is now part of HOL_ss. diff -r 61620d959717 -r 2757544bbe6d IMP/Equiv.ML --- 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-> 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;