| changeset 30988 | b53800e3ee47 |
| parent 30430 | 42ea5d85edcc |
| child 30989 | 1f39aea228b0 |
| 30987:2bbc22bd6a95 | 30988:b53800e3ee47 |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 header {*Well-founded Recursion*} |
7 header {*Well-founded Recursion*} |
8 |
8 |
9 theory Wellfounded |
9 theory Wellfounded |
10 imports Finite_Set Transitive_Closure Nat |
10 imports Finite_Set Wellfounded Nat |
11 uses ("Tools/function_package/size.ML") |
11 uses ("Tools/function_package/size.ML") |
12 begin |
12 begin |
13 |
13 |
14 subsection {* Basic Definitions *} |
14 subsection {* Basic Definitions *} |
15 |
15 |