equal
deleted
inserted
replaced
1 (* Title: HOL/Recdef.thy |
1 (* Title: HOL/Recdef.thy |
2 ID: $Id$ |
|
3 Author: Konrad Slind and Markus Wenzel, TU Muenchen |
2 Author: Konrad Slind and Markus Wenzel, TU Muenchen |
4 *) |
3 *) |
5 |
4 |
6 header {* TFL: recursive function definitions *} |
5 header {* TFL: recursive function definitions *} |
7 |
6 |
8 theory Recdef |
7 theory Recdef |
9 imports FunDef |
8 imports FunDef Plain |
10 uses |
9 uses |
11 ("Tools/TFL/casesplit.ML") |
10 ("Tools/TFL/casesplit.ML") |
12 ("Tools/TFL/utils.ML") |
11 ("Tools/TFL/utils.ML") |
13 ("Tools/TFL/usyntax.ML") |
12 ("Tools/TFL/usyntax.ML") |
14 ("Tools/TFL/dcterm.ML") |
13 ("Tools/TFL/dcterm.ML") |