repaired critical proofs depending on the order inside non-confluent SimpSets,

--- a/src/ZF/Resid/Cube.ML	Tue Apr 23 17:11:23 1996 +0200
+++ b/src/ZF/Resid/Cube.ML	Tue Apr 23 17:11:44 1996 +0200
@@ -54,10 +54,17 @@
 by (res_inst_tac [("u2","u"),("v2","v")](preservation RS ssubst) 1 
     THEN assume_tac 1 THEN assume_tac 1);
 by (res_inst_tac [("u2","v"),("v2","u")](preservation RS ssubst) 1);
-by (ALLGOALS(asm_full_simp_tac (res1_ss addsimps 
-    [prism RS sym,union_r,union_l,union_preserve_comp,union_preserve_regular,
-     read_instantiate [("u2","w"),("x1","v")] comp_trans,comp_sym_iff,
-     union_sym])));
+by (etac comp_sym 1);
+by (atac 1);
+by(rtac (prism RS sym RS ssubst) 1);
+by (asm_full_simp_tac (res1_ss addsimps 
+    [prism RS sym,union_l,union_preserve_regular,
+     comp_sym_iff, union_sym]) 4);
+by (asm_full_simp_tac (res1_ss addsimps [union_r, comp_sym_iff]) 1);
+by (asm_full_simp_tac (res1_ss addsimps 
+    [union_preserve_regular, comp_sym_iff]) 1);
+by (etac comp_trans 1);
+by (atac 1);
 val cube = result();
 
 
@@ -72,6 +79,16 @@
 by (forw_inst_tac [("x1","v")] (comp_sym RS comp_trans) 1);
 by (REPEAT(step_tac ZF_cs 1));
 by (rtac cube 1);
-by (ALLGOALS(asm_simp_tac (prism_ss addsimps [comp_sym_iff])));
+by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1);
+by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1);
+by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1);
+by (atac 1);
+by (etac (residuals_preserve_comp RS spec RS mp RS mp RS mp) 1);
+ by(atac 1);
+ by(etac comp_sym 1);
+ by(atac 1);
+by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1);
+by (asm_simp_tac prism_ss 1);
+by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1);
 val paving = result();
 

--- a/src/ZF/ex/Integ.ML	Tue Apr 23 17:11:23 1996 +0200
+++ b/src/ZF/ex/Integ.ML	Tue Apr 23 17:11:44 1996 +0200
@@ -384,9 +384,8 @@
     "!!z1 z2 z3. [| z1: integ;  z2: integ;  w: integ |] ==> \
 \                (z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
 by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac 
-    (intrel_ss addsimps ([zadd, zmult, add_mult_distrib] @ 
-                         add_ac @ mult_ac)) 1);
+by (asm_simp_tac (intrel_ss addsimps [zadd, zmult, add_mult_distrib]) 1);
+by (asm_simp_tac (intrel_ss addsimps (add_ac @ mult_ac)) 1);
 qed "zadd_zmult_distrib";
 
 val integ_typechecks =

--- a/src/ZF/ex/Limit.ML	Tue Apr 23 17:11:23 1996 +0200
+++ b/src/ZF/ex/Limit.ML	Tue Apr 23 17:11:44 1996 +0200
@@ -2167,9 +2167,9 @@
      add_type::nat_into_Ord::prems)) 1);
 by (etac lt_asym 1);
 by (assume_tac 1);
+by (asm_full_simp_tac (ZF_ss addsimps add_succ_right::succ_le_iff::prems) 1);
 by (asm_full_simp_tac (ZF_ss addsimps 
-    (succ_le_iff::add_succ::add_succ_right::le_iff::
-     add_type::nat_into_Ord::prems)) 1);
+    (add_succ::le_iff::add_type::nat_into_Ord::prems)) 1);
 by (safe_tac lemmas_cs);
 by (etac lt_irrefl 1);
 val add_le_elim1 = result();