equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 header {* More on Well-Founded Relations (FP) *} |
8 header {* More on Well-Founded Relations (FP) *} |
9 |
9 |
10 theory Wellfounded_More_FP |
10 theory Wellfounded_More_FP |
11 imports Wfrec Order_Relation_More_FP |
11 imports Wfrec Order_Relation |
12 begin |
12 begin |
13 |
13 |
14 |
14 |
15 text {* This section contains some variations of results in the theory |
15 text {* This section contains some variations of results in the theory |
16 @{text "Wellfounded.thy"}: |
16 @{text "Wellfounded.thy"}: |