| changeset 35727 | 817b8e0f7086 |
| parent 35719 | 99b6152aedf5 |
| child 35828 | 46cfc4b8112e |
| 35726:059d2f7b979f | 35727:817b8e0f7086 |
|---|---|
6 *) |
6 *) |
7 |
7 |
8 header {*Well-founded Recursion*} |
8 header {*Well-founded Recursion*} |
9 |
9 |
10 theory Wellfounded |
10 theory Wellfounded |
11 imports Transitive_Closure Big_Operators |
11 imports Transitive_Closure |
12 uses ("Tools/Function/size.ML") |
12 uses ("Tools/Function/size.ML") |
13 begin |
13 begin |
14 |
14 |
15 subsection {* Basic Definitions *} |
15 subsection {* Basic Definitions *} |
16 |
16 |