--- a/src/CCL/Lfp.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Lfp.ML Fri Oct 10 17:10:12 1997 +0200
@@ -45,7 +45,7 @@
val [lfp,mono,indhyp] = goal Lfp.thy
"[| a: lfp(f); mono(f); \
-\ !!x. [| x: f(lfp(f) Int {x.P(x)}) |] ==> P(x) \
+\ !!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x) \
\ |] ==> P(a)";
by (res_inst_tac [("a","a")] (Int_lower2 RS subsetD RS CollectD) 1);
by (rtac (lfp RSN (2, lfp_lowerbound RS subsetD)) 1);
@@ -64,7 +64,7 @@
val rew::prems = goal Lfp.thy
"[| A == lfp(f); a:A; mono(f); \
-\ !!x. [| x: f(A Int {x.P(x)}) |] ==> P(x) \
+\ !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x) \
\ |] ==> P(a)";
by (EVERY1 [rtac induct, (*backtracking to force correct induction*)
REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]);