1.1 --- a/src/HOL/Relation.thy	Tue Jul 10 17:30:49 2007 +0200
     1.2 +++ b/src/HOL/Relation.thy	Tue Jul 10 17:30:50 2007 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Relations *}
     1.5  
     1.6  theory Relation
     1.7 -imports Product_Type
     1.8 +imports Product_Type FixedPoint
     1.9  begin
    1.10  
    1.11  subsection {* Definitions *}
    1.12 @@ -529,4 +529,10 @@
    1.13    apply blast
    1.14    done
    1.15  
    1.16 +
    1.17 +subsection {* Version of @{text lfp_induct} for binary relations *}
    1.18 +
    1.19 +lemmas lfp_induct2 = 
    1.20 +  lfp_induct_set [of "(a, b)", split_format (complete)]
    1.21 +
    1.22  end