# HG changeset patch
# User haftmann
# Date 1184081450 -7200
# Node ID fd31da8f752a9ec44e1a49986aad1bd6b8f1c8e6
# Parent  b5eb0b4dd17d92c1f1dff4cdd5f59c6d3be9e91f
moved lfp_induct2 here

diff -r b5eb0b4dd17d -r fd31da8f752a 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