# HG changeset patch
# User paulson
# Date 916747195 -3600
# Node ID 7d38744313c8f39cd87e4eb24463abd12cf7cc3e
# Parent  1eb364a68c5469ad8ae1a7c9fa7034ed4c4653aa
tidied freeness reasoning

diff -r 1eb364a68c54 -r 7d38744313c8 src/ZF/ex/BT.ML
--- a/src/ZF/ex/BT.ML	Tue Jan 19 12:56:27 1999 +0100
+++ b/src/ZF/ex/BT.ML	Tue Jan 19 12:59:55 1999 +0100
@@ -10,7 +10,7 @@
 
 Goal "l : bt(A) ==> ALL x r. Br(x,l,r) ~= l";
 by (induct_tac "l" 1);
-by (ALLGOALS Asm_full_simp_tac);
+by Auto_tac;
 qed_spec_mp "Br_neq_left";
 
 (*Proving a freeness theorem*)
diff -r 1eb364a68c54 -r 7d38744313c8 src/ZF/ex/Comb.ML
--- a/src/ZF/ex/Comb.ML	Tue Jan 19 12:56:27 1999 +0100
+++ b/src/ZF/ex/Comb.ML	Tue Jan 19 12:59:55 1999 +0100
@@ -40,7 +40,6 @@
 val Ap_E = comb.mk_cases "p#q : comb";
 
 AddSIs comb.intrs;
-AddSEs comb.free_SEs;
 
 
 (*** Results about Contraction ***)
@@ -87,11 +86,11 @@
 AddSEs [K_contractE, S_contractE, Ap_contractE];
 
 Goalw [I_def] "I -1-> r ==> P";
-by (Blast_tac 1);
+by Auto_tac;
 qed "I_contract_E";
 
 Goal "K#p -1-> r ==> (EX q. r = K#q & p -1-> q)";
-by (Blast_tac 1);
+by Auto_tac;
 qed "K1_contractD";
 
 Goal "[| p ---> q;  r: comb |] ==> p#r ---> q#r";
@@ -156,31 +155,34 @@
 (*** Basic properties of parallel contraction ***)
 
 Goal "K#p =1=> r ==> (EX p'. r = K#p' & p =1=> p')";
-by (Blast_tac 1);
+by Auto_tac;
 qed "K1_parcontractD";
+AddSDs [K1_parcontractD];
 
 Goal "S#p =1=> r ==> (EX p'. r = S#p' & p =1=> p')";
-by (Blast_tac 1);
+by Auto_tac;
 qed "S1_parcontractD";
+AddSDs [S1_parcontractD];
 
 Goal "S#p#q =1=> r ==> (EX p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')";
-by (blast_tac (claset() addSDs [S1_parcontractD]) 1);
+by Auto_tac;
 qed "S2_parcontractD";
+AddSDs [S2_parcontractD];
 
 (*Church-Rosser property for parallel contraction*)
 Goalw [diamond_def] "diamond(parcontract)";
 by (rtac (impI RS allI RS allI) 1);
 by (etac parcontract.induct 1);
 by (ALLGOALS 
-    (blast_tac (claset() addSDs [K1_parcontractD, S2_parcontractD]
-                        addIs  [parcontract_combD2])));
+    (blast_tac (claset() addSEs comb.free_SEs
+			 addIs [parcontract_combD2])));
 qed "diamond_parcontract";
 
 (*** Equivalence of p--->q and p===>q ***)
 
 Goal "p-1->q ==> p=1=>q";
 by (etac contract.induct 1);
-by (ALLGOALS Blast_tac);
+by Auto_tac;
 qed "contract_imp_parcontract";
 
 Goal "p--->q ==> p===>q";
@@ -189,7 +191,7 @@
 by (etac rtrancl_induct 1);
 by (blast_tac (claset() addIs [r_into_trancl]) 1);
 by (blast_tac (claset() addIs [contract_imp_parcontract, 
-			      r_into_trancl, trans_trancl RS transD]) 1);
+			       r_into_trancl, trans_trancl RS transD]) 1);
 qed "reduce_imp_parreduce";
 
 
@@ -200,8 +202,8 @@
 by (blast_tac (claset() addIs reduction_rls) 1);
 by (blast_tac 
     (claset() addIs [trans_rtrancl RS transD,
-		    Ap_reduce1, Ap_reduce2, parcontract_combD1,
-		    parcontract_combD2]) 1);
+		     Ap_reduce1, Ap_reduce2, parcontract_combD1,
+		     parcontract_combD2]) 1);
 qed "parcontract_imp_reduce";
 
 Goal "p===>q ==> p--->q";
@@ -214,7 +216,7 @@
 qed "parreduce_imp_reduce";
 
 Goal "p===>q <-> p--->q";
-by (REPEAT (ares_tac [iffI, parreduce_imp_reduce, reduce_imp_parreduce] 1));
+by (blast_tac (claset() addIs [parreduce_imp_reduce, reduce_imp_parreduce]) 1);
 qed "parreduce_iff_reduce";
 
 writeln"Reached end of file.";