src/ZF/QUniv.ML

--- a/src/ZF/QUniv.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/QUniv.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -20,7 +20,7 @@
 val [prem] = goalw QUniv.thy [sum_def]
     "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
 by (stac Int_Un_distrib 1);
-by (fast_tac (!claset addSDs [prem RS Transset_Pair_D]) 1);
+by (blast_tac (!claset addSDs [prem RS Transset_Pair_D]) 1);
 qed "Transset_sum_Int_subset";
 
 (** Introduction and elimination rules avoid tiresome folding/unfolding **)
@@ -187,13 +187,13 @@
 goalw Univ.thy [Pair_def]
     "!!X. [| <a,b> : Vfrom(X,succ(i));  Transset(X) |] ==> \
 \         a: Vfrom(X,i)  &  b: Vfrom(X,i)";
-by (fast_tac (!claset addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1);
+by (blast_tac (!claset addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1);
 qed "Pair_in_Vfrom_D";
 
 goal Univ.thy
  "!!X. Transset(X) ==>          \
 \      (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))";
-by (fast_tac (!claset addSDs [Pair_in_Vfrom_D]) 1);
+by (blast_tac (!claset addSDs [Pair_in_Vfrom_D]) 1);
 qed "product_Int_Vfrom_subset";
 
 (*** Intersecting <a;b> with Vfrom... ***)