# HG changeset patch
# User paulson
# Date 962187356 -7200
# Node ID a7ec0fef986097251c80573c6884bf9bb9d76065
# Parent  199b43f712af904520d5d28a4a7fe2a334810e31
fixed some weak elim rules, and tidied

diff -r 199b43f712af -r a7ec0fef9860 src/ZF/IMP/Equiv.ML
--- a/src/ZF/IMP/Equiv.ML	Wed Jun 28 12:15:28 2000 +0200
+++ b/src/ZF/IMP/Equiv.ML	Wed Jun 28 12:15:56 2000 +0200
@@ -65,17 +65,16 @@
 
 AddSIs [aexp2,bexp2,B_type,A_type];
 AddIs  evalc.intrs;
-AddEs  [C_type,C_type_fst];
 
 
 Goal "c : com ==> ALL x:C(c). <c,fst(x)> -c-> snd(x)";
 by (etac com.induct 1);
-(* skip *)
-by (fast_tac (claset() addss (simpset())) 1);
+(* comp *)
+by (Force_tac 3); 
 (* assign *)
-by (fast_tac (claset() addss (simpset())) 1);
-(* comp *)
-by (best_tac (claset() addss (simpset())) 1);
+by (Force_tac 2); 
+(* skip *)
+by (Force_tac 1); 
 (* while *)
 by Safe_tac;
 by (ALLGOALS Asm_full_simp_tac);