src/HOL/Finite.ML

--- a/src/HOL/Finite.ML	Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Finite.ML	Wed Apr 09 12:32:04 1997 +0200
@@ -16,7 +16,7 @@
 qed "Fin_mono";
 
 goalw Finite.thy Fin.defs "Fin(A) <= Pow(A)";
-by (fast_tac (!claset addSIs [lfp_lowerbound]) 1);
+by (blast_tac (!claset addSIs [lfp_lowerbound]) 1);
 qed "Fin_subset_Pow";
 
 (* A : Fin(B) ==> A <= B *)
@@ -55,7 +55,7 @@
 qed "Fin_subset";
 
 goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))";
-by (fast_tac (!claset addIs [Fin_UnI] addDs
+by (blast_tac (!claset addIs [Fin_UnI] addDs
                 [Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1);
 qed "subset_Fin";
 Addsimps[subset_Fin];
@@ -63,7 +63,7 @@
 goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)";
 by (stac insert_is_Un 1);
 by (Simp_tac 1);
-by (fast_tac (!claset addSIs Fin.intrs addDs [FinD]) 1);
+by (blast_tac (!claset addSIs Fin.intrs addDs [FinD]) 1);
 qed "insert_Fin";
 Addsimps[insert_Fin];
 
@@ -163,7 +163,7 @@
 section "Finite cardinality -- 'card'";
 
 goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 val Collect_conv_insert = result();
 
 goalw Finite.thy [card_def] "card {} = 0";
@@ -197,7 +197,7 @@
 by (case_tac "? a. a:A" 1);
  by (res_inst_tac [("x","0")] exI 2);
  by (Simp_tac 2);
- by (Fast_tac 2);
+ by (Blast_tac 2);
 by (etac exE 1);
 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
 by (rtac exI 1);
@@ -205,47 +205,47 @@
 by (etac equalityE 1);
 by (asm_full_simp_tac
      (!simpset addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);
-by (SELECT_GOAL(safe_tac (!claset))1);
+by (safe_tac (!claset));
   by (Asm_full_simp_tac 1);
   by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
   by (SELECT_GOAL(safe_tac (!claset))1);
    by (subgoal_tac "x ~= f m" 1);
-    by (Fast_tac 2);
+    by (Blast_tac 2);
    by (subgoal_tac "? k. f k = x & k<m" 1);
-    by (best_tac (!claset) 2);
+    by (Blast_tac 2);
    by (SELECT_GOAL(safe_tac (!claset))1);
    by (res_inst_tac [("x","k")] exI 1);
    by (Asm_simp_tac 1);
   by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-  by (best_tac (!claset) 1);
+  by (Blast_tac 1);
  bd sym 1;
  by (rotate_tac ~1 1);
  by (Asm_full_simp_tac 1);
  by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
  by (SELECT_GOAL(safe_tac (!claset))1);
   by (subgoal_tac "x ~= f m" 1);
-   by (Fast_tac 2);
+   by (Blast_tac 2);
   by (subgoal_tac "? k. f k = x & k<m" 1);
-   by (best_tac (!claset) 2);
+   by (Blast_tac 2);
   by (SELECT_GOAL(safe_tac (!claset))1);
   by (res_inst_tac [("x","k")] exI 1);
   by (Asm_simp_tac 1);
  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
- by (best_tac (!claset) 1);
+ by (Blast_tac 1);
 by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
 by (SELECT_GOAL(safe_tac (!claset))1);
  by (subgoal_tac "x ~= f i" 1);
-  by (Fast_tac 2);
+  by (Blast_tac 2);
  by (case_tac "x = f m" 1);
   by (res_inst_tac [("x","i")] exI 1);
   by (Asm_simp_tac 1);
  by (subgoal_tac "? k. f k = x & k<m" 1);
-  by (best_tac (!claset) 2);
+  by (Blast_tac 2);
  by (SELECT_GOAL(safe_tac (!claset))1);
  by (res_inst_tac [("x","k")] exI 1);
  by (Asm_simp_tac 1);
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by (best_tac (!claset) 1);
+by (Blast_tac 1);
 val lemma = result();
 
 goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
@@ -303,8 +303,8 @@
 by (Asm_simp_tac 1);
 by (rtac card_insert_disjoint 1);
 by (rtac (major RSN (2,finite_subset)) 1);
-by (Fast_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
 by (asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1);
 qed "card_insert";
 Addsimps [card_insert];