--- a/src/HOL/Lfp.ML Wed Jul 17 16:03:42 1996 +0200
+++ b/src/HOL/Lfp.ML Wed Jul 17 17:12:33 1996 +0200
@@ -56,12 +56,6 @@
Prod_Syntax.split_rule
(read_instantiate [("a","(a,b)")] induct));
-(*** Fixpoint induction a la David Park ***)
-goal Lfp.thy "!!f. [| mono f; f A <= A |] ==> lfp(f) <= A";
-by (rtac subsetI 1);
-by (EVERY[etac induct 1, atac 1, etac subsetD 1, rtac subsetD 1,
- atac 2, fast_tac (!claset addSEs [monoD]) 1]);
-qed "Park_induct";
(** Definition forms of lfp_Tarski and induct, to control unfolding **)