diff -r d9527f97246e -r 89669c58e506 Gfp.ML
--- 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);