src/ZF/Fixedpt.ML

 (**** Proof of Knaster-Tarski Theorem for the lfp ****)
 
 (*lfp is contained in each pre-fixedpoint*)
 goalw Fixedpt.thy [lfp_def]
     "!!A. [| h(A) <= A;  A<=D |] ==> lfp(D,h) <= A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 (*or  by (rtac (PowI RS CollectI RS Inter_lower) 1); *)
 qed "lfp_lowerbound";
 
 (*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*)
 goalw Fixedpt.thy [lfp_def,Inter_def] "lfp(D,h) <= D";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "lfp_subset";
 
 (*Used in datatype package*)
 val [rew] = goal Fixedpt.thy "A==lfp(D,h) ==> A <= D";
 by (rewtac rew);

 by (rtac (PowI RS CollectI RS Union_upper) 1);
 by (REPEAT (resolve_tac prems 1));
 qed "gfp_upperbound";
 
 goalw Fixedpt.thy [gfp_def] "gfp(D,h) <= D";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "gfp_subset";
 
 (*Used in datatype package*)
 val [rew] = goal Fixedpt.thy "A==gfp(D,h) ==> A <= D";
 by (rewtac rew);