src/ZF/QUniv.ML

 qed "Transset_includes_summands";
 
 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 **)
 
 goalw QUniv.thy [quniv_def]

 **)
 
 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... ***)
 
 goalw QUniv.thy [QPair_def,sum_def]