# HG changeset patch
# User pusch
# Date 837616353 -7200
# Node ID b07ee188f06124e37bcf2b1369034073172362c7
# Parent  206553e1a242d5c6b2b21262bf89983acf08264a
removed superfluous Park-induct rule

diff -r 206553e1a242 -r b07ee188f061 src/HOL/Lfp.ML
--- 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 **)