--- a/src/ZF/Fixedpt.ML Fri Jan 03 10:48:28 1997 +0100
+++ b/src/ZF/Fixedpt.ML Fri Jan 03 15:01:55 1997 +0100
@@ -56,13 +56,13 @@
(*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 ZF_cs 1);
+by (Fast_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 ZF_cs 1);
+by (Fast_tac 1);
qed "lfp_subset";
(*Used in datatype package*)
@@ -190,7 +190,7 @@
qed "gfp_upperbound";
goalw Fixedpt.thy [gfp_def] "gfp(D,h) <= D";
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
qed "gfp_subset";
(*Used in datatype package*)