equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 header {* Relations *} |
7 header {* Relations *} |
8 |
8 |
9 theory Relation |
9 theory Relation |
10 imports Product_Type |
10 imports Product_Type FixedPoint |
11 begin |
11 begin |
12 |
12 |
13 subsection {* Definitions *} |
13 subsection {* Definitions *} |
14 |
14 |
15 definition |
15 definition |
527 apply (unfold trans_def inv_image_def) |
527 apply (unfold trans_def inv_image_def) |
528 apply (simp (no_asm)) |
528 apply (simp (no_asm)) |
529 apply blast |
529 apply blast |
530 done |
530 done |
531 |
531 |
|
532 |
|
533 subsection {* Version of @{text lfp_induct} for binary relations *} |
|
534 |
|
535 lemmas lfp_induct2 = |
|
536 lfp_induct_set [of "(a, b)", split_format (complete)] |
|
537 |
532 end |
538 end |