--- a/Gfp.ML Thu Aug 25 10:47:33 1994 +0200
+++ b/Gfp.ML Thu Aug 25 11:01:45 1994 +0200
@@ -113,6 +113,15 @@
by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct]) 1));
val def_coinduct = result();
+(*The version used in the induction/coinduction package*)
+val prems = goal Gfp.thy
+ "[| A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w))); \
+\ a: X; !!z. z: X ==> P(X Un A, z) |] ==> \
+\ a : A";
+by (rtac def_coinduct 1);
+by (REPEAT (ares_tac (prems @ [subsetI,CollectI]) 1));
+val def_Collect_coinduct = result();
+
val rew::prems = goal Gfp.thy
"[| A==gfp(f); mono(f); a:X; X <= f(lfp(%x.f(x) Un X Un A)) |] ==> a: A";
by (rewtac rew);