Lfp.ML

--- a/Lfp.ML	Thu Aug 25 10:47:33 1994 +0200
+++ b/Lfp.ML	Thu Aug 25 11:01:45 1994 +0200
@@ -60,7 +60,7 @@
 val def_lfp_Tarski = result();
 
 val rew::prems = goal Lfp.thy
-    "[| A == lfp(f);  a:A;  mono(f);   			\
+    "[| A == lfp(f);  mono(f);   a:A;  			\
 \       !!x. [| x: f(A Int {x.P(x)}) |] ==> P(x) 	\
 \    |] ==> P(a)";
 by (EVERY1 [rtac induct,	(*backtracking to force correct induction*)