changeset 23709 | fd31da8f752a |
parent 23185 | 1fa87978cf27 |
child 24286 | 7619080e49f0 |
--- 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