equal
deleted
inserted
replaced
8 header {* More on Well-Founded Relations *} |
8 header {* More on Well-Founded Relations *} |
9 |
9 |
10 theory Wellfounded_More |
10 theory Wellfounded_More |
11 imports Wellfounded Order_Relation_More |
11 imports Wellfounded Order_Relation_More |
12 begin |
12 begin |
13 |
|
14 |
13 |
15 subsection {* Well-founded recursion via genuine fixpoints *} |
14 subsection {* Well-founded recursion via genuine fixpoints *} |
16 |
15 |
17 (*2*)lemma adm_wf_unique_fixpoint: |
16 (*2*)lemma adm_wf_unique_fixpoint: |
18 fixes r :: "('a * 'a) set" and |
17 fixes r :: "('a * 'a) set" and |