src/HOL/Relation.thy

--- a/src/HOL/Relation.thy	Tue Jul 10 17:30:49 2007 +0200
+++ b/src/HOL/Relation.thy	Tue Jul 10 17:30:50 2007 +0200
@@ -7,7 +7,7 @@
 header {* Relations *}
 
 theory Relation
-imports Product_Type
+imports Product_Type FixedPoint
 begin
 
 subsection {* Definitions *}
@@ -529,4 +529,10 @@
   apply blast
   done
 
+
+subsection {* Version of @{text lfp_induct} for binary relations *}
+
+lemmas lfp_induct2 = 
+  lfp_induct_set [of "(a, b)", split_format (complete)]
+
 end