Now calls blast_tac

--- a/src/HOL/Lambda/Commutation.ML	Fri Apr 04 11:33:51 1997 +0200
+++ b/src/HOL/Lambda/Commutation.ML	Fri Apr 04 12:21:28 1997 +0200
@@ -11,25 +11,25 @@
 (*** square ***)
 
 goalw Commutation.thy [square_def] "!!R. square R S T U ==> square S R U T";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "square_sym";
 
 goalw Commutation.thy [square_def]
   "!!R. [| square R S T U; T <= T' |] ==> square R S T' U";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "square_subset";
 
 goalw Commutation.thy [square_def]
   "!!R. [| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "square_reflcl";
 
 goalw Commutation.thy [square_def]
   "!!R. square R S S T ==> square (R^*) S S (T^*)";
 by (strip_tac 1);
 by (etac rtrancl_induct 1);
-by (Fast_tac 1);
-by (best_tac (!claset addSEs [rtrancl_into_rtrancl]) 1);
+by (Blast_tac 1);
+by (blast_tac (!claset addIs [rtrancl_into_rtrancl]) 1);
 qed "square_rtrancl";
 
 goalw Commutation.thy [commute_def]
@@ -42,16 +42,16 @@
 (*** commute ***)
 
 goalw Commutation.thy [commute_def] "!!R. commute R S ==> commute S R";
-by (fast_tac (!claset addIs [square_sym]) 1);
+by (blast_tac (!claset addIs [square_sym]) 1);
 qed "commute_sym";
 
 goalw Commutation.thy [commute_def] "!!R. commute R S ==> commute (R^*) (S^*)";
-by (fast_tac (!claset addIs [square_rtrancl,square_sym]) 1);
+by (blast_tac (!claset addIs [square_rtrancl,square_sym]) 1);
 qed "commute_rtrancl";
 
 goalw Commutation.thy [commute_def,square_def]
   "!!R. [| commute R T; commute S T |] ==> commute (R Un S) T";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "commute_Un";
 
 (*** diamond, confluence and union ***)
@@ -67,15 +67,15 @@
 
 goalw Commutation.thy [diamond_def]
   "!!R. square R R (R^=) (R^=) ==> confluent R";
-by (fast_tac (!claset addIs [square_rtrancl_reflcl_commute,r_into_rtrancl]
-                       addEs [square_subset]) 1);
+by (fast_tac (!claset addIs [square_rtrancl_reflcl_commute, r_into_rtrancl]
+                      addEs [square_subset]) 1);
 qed "square_reflcl_confluent";
 
 goal Commutation.thy
  "!!R. [| confluent R; confluent S; commute (R^*) (S^*) |] \
 \      ==> confluent(R Un S)";
 by (rtac (rtrancl_Un_rtrancl RS subst) 1);
-by (fast_tac (!claset addDs [diamond_Un] addIs [diamond_confluent]) 1);
+by (blast_tac (!claset addDs [diamond_Un] addIs [diamond_confluent]) 1);
 qed "confluent_Un";
 
 goal Commutation.thy
@@ -88,13 +88,12 @@
 
 goalw Commutation.thy [square_def,commute_def,diamond_def,Church_Rosser_def]
   "Church_Rosser(R) = confluent(R)";
-by (rtac iffI 1);
- by (fast_tac (HOL_cs addIs
+by (safe_tac HOL_cs);
+ by (blast_tac (HOL_cs addIs
       [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
        rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
-by (safe_tac HOL_cs);
 by (etac rtrancl_induct 1);
- by (Fast_tac 1);
+ by (Blast_tac 1);
 by (slow_best_tac (!claset addIs [r_into_rtrancl]
                     addEs [rtrancl_trans,r_into_rtrancl RS rtrancl_trans]) 1);
 qed "Church_Rosser_confluent";