diff -r bf044f0db994 -r 96c68fd7ed46 IMP/Equiv.ML
--- a/IMP/Equiv.ML	Tue Sep 06 16:46:27 1994 +0200
+++ b/IMP/Equiv.ML	Wed Sep 07 13:17:34 1994 +0200
@@ -16,20 +16,25 @@
 val aexp2 = aexp_iff RS iffD2;
 
 
+goal Equiv.thy "!w. (<b,s> -b-> w) --> (B(b,s) = w)";
+by (bexp.induct_tac "b" 1);
+by (rewrite_goals_tac B_simps);		(*denotational semantics*)
+by (ALLGOALS (fast_tac (HOL_cs addSDs [aexp1] addSEs bexp_elim_cases)));
+val bexp_imp1 = result();
+
+goal Equiv.thy "!w. (B(b,s) = w) --> (<b,s> -b-> w)";
+by (bexp.induct_tac "b" 1);
+by (rewrite_goals_tac B_simps);		(*denotational semantics*)
+by (ALLGOALS (best_tac (HOL_cs addSIs (aexp2::evalb.intrs))));
+val bexp_imp2 = result();
+
+val bexp1 = bexp_imp1 RS spec RS mp |> standard;
+val bexp2 = bexp_imp2 RS spec RS mp |> standard;
+
 goal Equiv.thy "(<b,s> -b-> w) = (B(b,s) = w)";
-by (res_inst_tac [("x","w")] spec 1);			(* quantify w *)
-by (bexp.induct_tac "b" 1);		                (* struct. ind. *)
-by(rewrite_goals_tac B_simps);
-  (* simplification with HOL_ss too agressive: (True=x) == True *)
-by (safe_tac (HOL_cs addSIs (aexp2::evalb.intrs)
-                     addSDs [aexp1] addSEs bexp_elim_cases)
-    THEN ALLGOALS(best_tac HOL_cs));
-
+by (fast_tac (HOL_cs addSEs [bexp1,bexp2]) 1);
 val bexp_iff = result();
 
-val bexp1 = bexp_iff RS iffD1;
-val bexp2 = bexp_iff RS iffD2;
-
 val BfstI = read_instantiate_sg (sign_of Equiv.thy)
               [("P","%x.B(?b,x)")] (fst_conv RS ssubst);
 val BfstD = read_instantiate_sg (sign_of Equiv.thy)