# HG changeset patch
# User paulson
# Date 880561572 -3600
# Node ID c872cc541db2ebb2fa9ba638f7c24c9a19d2fd32
# Parent  2c99775d953fe7edebdecca5e4cd692ffb7d4331
Tidying and modification to cope with iffCE

diff -r 2c99775d953f -r c872cc541db2 src/HOL/IMP/Expr.ML
--- a/src/HOL/IMP/Expr.ML	Wed Nov 26 17:23:18 1997 +0100
+++ b/src/HOL/IMP/Expr.ML	Wed Nov 26 17:26:12 1997 +0100
@@ -32,15 +32,16 @@
    "((b0 ori b1,sigma) -b-> w) = \
 \   (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"];
 
-goal Expr.thy "!n. ((a,s) -a-> n) = (n = A a s)";
-by (aexp.induct_tac "a" 1);                               (* struct. ind. *)
-by (ALLGOALS Simp_tac);                                   (* rewr. Den.   *)
-by (TRYALL (fast_tac (claset() addSIs (evala.intrs@prems)
-                             addSEs evala_elim_cases)));
+goal Expr.thy "!n. ((a,s) -a-> n) = (A a s = n)";
+by (aexp.induct_tac "a" 1);
+by (ALLGOALS 
+    (fast_tac (claset() addSIs evala.intrs
+	                addSEs evala_elim_cases addss (simpset()))));
 qed_spec_mp "aexp_iff";
 
-goal Expr.thy "!w. ((b,s) -b-> w) = (w = B b s)";
+goal Expr.thy "!w. ((b,s) -b-> w) = (B b s = w)";
 by (bexp.induct_tac "b" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addcongs [conj_cong]
-                                    addsimps (aexp_iff::evalb_simps))));
+by (ALLGOALS 
+    (fast_tac (claset() 
+	       addss (simpset() addsimps (aexp_iff::evalb_simps)))));
 qed_spec_mp "bexp_iff";