# HG changeset patch
# User haftmann
# Date 1184081447 -7200
# Node ID 745799215e02371864ac98e01897c7be558290d5
# Parent  b7abba3c230ed47841f1f832686e041a5ad3edf1
moved lfp_induct2 to Relation.thy

diff -r b7abba3c230e -r 745799215e02 src/HOL/FixedPoint.thy
--- a/src/HOL/FixedPoint.thy	Tue Jul 10 17:30:45 2007 +0200
+++ b/src/HOL/FixedPoint.thy	Tue Jul 10 17:30:47 2007 +0200
@@ -8,7 +8,7 @@
 header {* Fixed Points and the Knaster-Tarski Theorem*}
 
 theory FixedPoint
-imports Product_Type
+imports Fun
 begin
 
 subsection {* Complete lattices *}
@@ -330,9 +330,6 @@
   by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
     (auto simp: inf_set_eq intro: indhyp)
 
-text {* Version of induction for binary relations *}
-lemmas lfp_induct2 =  lfp_induct_set [of "(a, b)", split_format (complete)]
-
 lemma lfp_ordinal_induct: 
   assumes mono: "mono f"
   shows "[| !!S. P S ==> P(f S); !!M. !S:M. P S ==> P(Union M) |] 
@@ -496,7 +493,6 @@
 val lfp_greatest = thm "lfp_greatest";
 val lfp_unfold = thm "lfp_unfold";
 val lfp_induct = thm "lfp_induct";
-val lfp_induct2 = thm "lfp_induct2";
 val lfp_ordinal_induct = thm "lfp_ordinal_induct";
 val def_lfp_unfold = thm "def_lfp_unfold";
 val def_lfp_induct = thm "def_lfp_induct";