src/ZF/Resid/Reduction.ML

--- a/src/ZF/Resid/Reduction.ML	Mon Sep 21 23:25:27 1998 +0200
+++ b/src/ZF/Resid/Reduction.ML	Tue Sep 22 13:48:32 1998 +0200
@@ -31,7 +31,6 @@
 	  [Spar_red.one_step, substL_type, redD1, redD2, par_redD1, 
 	   par_redD2, par_red1D2, unmark_type]);
 
-val reducL_ss = simpset() setloop (SELECT_GOAL Safe_tac);
 
 (* ------------------------------------------------------------------------- *)
 (*     Lemmas for reduction                                                  *)
@@ -73,7 +72,7 @@
 
 
 Goal "m:lambda==> m =1=> m";
-by (eresolve_tac [lambda.induct] 1);
+by (etac lambda.induct 1);
 by (ALLGOALS (Asm_simp_tac ));
 qed "refl_par_red1";
 
@@ -113,17 +112,16 @@
 (*           commuting of unmark and subst                                   *)
 (* ------------------------------------------------------------------------- *)
 
-Goal "u:redexes ==> \
-\           ALL k:nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)";
-by (eresolve_tac [redexes.induct] 1);
-by (ALLGOALS (asm_full_simp_tac (addsplit (simpset()))));
+Goal "u:redexes ==> ALL k:nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)";
+by (etac redexes.induct 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var])));
 qed "unmmark_lift_rec";
 
 Goal "v:redexes ==> ALL k:nat. ALL u:redexes.  \
 \         unmark(subst_rec(u,v,k)) = subst_rec(unmark(u),unmark(v),k)";
-by (eresolve_tac [redexes.induct] 1);
-by (ALLGOALS (asm_full_simp_tac 
-             ((addsplit (simpset())) addsimps [unmmark_lift_rec])));
+by (etac redexes.induct 1);
+by (ALLGOALS (asm_simp_tac 
+	      (simpset() addsimps [unmmark_lift_rec, subst_Var])));
 qed "unmmark_subst_rec";
 
 
@@ -133,9 +131,10 @@
 
 Goal "u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)";
 by (etac Scomp.induct 1);
-by (ALLGOALS (asm_full_simp_tac (reducL_ss addsimps [unmmark_subst_rec]) ));
+by (auto_tac (claset(),
+	      simpset() addsimps [unmmark_subst_rec]));
 by (dres_inst_tac [("psi", "Fun(?u) =1=> ?w")] asm_rl 1);
-by (asm_full_simp_tac reducL_ss 1);
+by Auto_tac;
 qed_spec_mp "completeness_l";
 
 Goal "[|u:lambda; u~v; regular(v)|]==> u =1=> unmark(u|>v)";