# HG changeset patch
# User paulson
# Date 860146431 -7200
# Node ID 86cc7ef9b30c0e4cbedc5c64fc386727dfb12a71
# Parent  c1a00adb0a80df76fc3830edf9638745a72d8442
Another blast_tac call

diff -r c1a00adb0a80 -r 86cc7ef9b30c src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Fri Apr 04 11:32:44 1997 +0200
+++ b/src/ZF/Cardinal.ML	Fri Apr 04 11:33:51 1997 +0200
@@ -748,7 +748,7 @@
 by (asm_full_simp_tac (!simpset addsimps [wf_on_def, wf_def, Memrel_iff]) 1);
 by (excluded_middle_tac "x:Z" 1);
 by (dres_inst_tac [("x", "x")] bspec 2 THEN assume_tac 2);
-by (fast_tac (!claset addSEs [mem_irrefl] addEs [mem_asym]) 2);
+by (blast_tac (!claset addEs [mem_irrefl, mem_asym]) 2);
 by (dres_inst_tac [("x", "Z")] spec 1);
 by (Blast.depth_tac (!claset) 4 1);
 qed "nat_wf_on_converse_Memrel";
diff -r c1a00adb0a80 -r 86cc7ef9b30c src/ZF/ex/Mutil.ML
--- a/src/ZF/ex/Mutil.ML	Fri Apr 04 11:32:44 1997 +0200
+++ b/src/ZF/ex/Mutil.ML	Fri Apr 04 11:33:51 1997 +0200
@@ -71,7 +71,7 @@
 by (simp_tac (!simpset addsimps tiling.intrs) 1);
 by (asm_full_simp_tac (!simpset addsimps [Un_assoc,
 					  subset_empty_iff RS iff_sym]) 1);
-by (fast_tac (!claset addIs tiling.intrs) 1);
+by (blast_tac (!claset addIs tiling.intrs) 1);
 bind_thm ("tiling_UnI", result() RS mp RS mp);
 
 goal thy "!!t. t:tiling(domino) ==> Finite(t)";
@@ -87,7 +87,7 @@
 by (Simp_tac 2 THEN assume_tac 1);
 by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
 by (Simp_tac 2 THEN assume_tac 1);
-by (step_tac (!claset) 1);
+by (Step_tac 1);
 by (subgoal_tac "ALL p b. p:evnodd(a,b) --> p~:evnodd(ta,b)" 1);
 by (asm_simp_tac (!simpset addsimps [evnodd_Un, Un_cons, tiling_domino_Finite,
                                   evnodd_subset RS subset_Finite,