Adapted proofs because of new simplification tactics.

--- a/src/ZF/AC/DC.ML	Tue Mar 10 19:02:20 1998 +0100
+++ b/src/ZF/AC/DC.ML	Tue Mar 10 19:02:53 1998 +0100
@@ -406,7 +406,7 @@
                      addSIs [UN_image_succ_eq_succ] addss (simpset())) 1);
 by (etac conjE 1);
 by (etac notE 1);
-by (asm_full_simp_tac (simpset() addsimps [UN_image_succ_eq_succ]) 1);
+by (asm_lr_simp_tac (simpset() addsimps [UN_image_succ_eq_succ]) 1);
 (** LEVEL 12 **)
 by (REPEAT (eresolve_tac [conjE, bexE] 1));
 by (dtac apply_domain_type 1 THEN REPEAT (assume_tac 1));
@@ -607,5 +607,4 @@
 by (asm_full_simp_tac (simpset()
         addsimps [[Card_is_Ord, ltD] MRS lam_images_eq]) 1);
 by (fast_tac (claset() addSEs [ltE, lemma RS CollectD2]) 1);
-qed" WO1_DC_Card";
-
+qed "WO1_DC_Card";

--- a/src/ZF/Resid/Substitution.ML	Tue Mar 10 19:02:20 1998 +0100
+++ b/src/ZF/Resid/Substitution.ML	Tue Mar 10 19:02:53 1998 +0100
@@ -199,7 +199,6 @@
 by (forward_tac  [lt_trans1] 1 THEN assume_tac 1);
 by (ALLGOALS(asm_full_simp_tac 
              (simpset() addsimps [succ_pred,leI,gt_pred])));
-by (hyp_subst_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [leI]) 1);
 by (excluded_middle_tac "na < xa" 1);
 by (asm_full_simp_tac (simpset()) 1);

--- a/src/ZF/ex/Mutil.ML	Tue Mar 10 19:02:20 1998 +0100
+++ b/src/ZF/ex/Mutil.ML	Tue Mar 10 19:02:53 1998 +0100
@@ -131,7 +131,7 @@
                                   dominoes_tile_matrix]) 2);
 by (subgoal_tac "(m#+m)#+(n#+n) = (m#+n)#+(m#+n)" 1);
 by (asm_simp_tac (simpset() addsimps add_ac) 2);
-by (asm_full_simp_tac 
+by (asm_lr_simp_tac 
     (simpset() addsimps [evnodd_Diff, mod2_add_self,
                         mod2_succ_succ, tiling_domino_0_1 RS sym]) 1);
 by (rtac lt_trans 1);