equal
deleted
inserted
replaced
3 Author: Konrad Slind and Markus Wenzel, TU Muenchen |
3 Author: Konrad Slind and Markus Wenzel, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* TFL: recursive function definitions *} |
6 header {* TFL: recursive function definitions *} |
7 |
7 |
8 theory Recdef = Wellfounded_Relations + Datatype |
8 theory Recdef |
|
9 import Wellfounded_Relations Datatype |
9 files |
10 files |
10 ("../TFL/utils.ML") |
11 ("../TFL/utils.ML") |
11 ("../TFL/usyntax.ML") |
12 ("../TFL/usyntax.ML") |
12 ("../TFL/dcterm.ML") |
13 ("../TFL/dcterm.ML") |
13 ("../TFL/thms.ML") |
14 ("../TFL/thms.ML") |
14 ("../TFL/rules.ML") |
15 ("../TFL/rules.ML") |
15 ("../TFL/thry.ML") |
16 ("../TFL/thry.ML") |
16 ("../TFL/tfl.ML") |
17 ("../TFL/tfl.ML") |
17 ("../TFL/post.ML") |
18 ("../TFL/post.ML") |
18 ("Tools/recdef_package.ML"): |
19 ("Tools/recdef_package.ML") |
|
20 begin |
19 |
21 |
20 lemma tfl_eq_True: "(x = True) --> x" |
22 lemma tfl_eq_True: "(x = True) --> x" |
21 by blast |
23 by blast |
22 |
24 |
23 lemma tfl_rev_eq_mp: "(x = y) --> y --> x"; |
25 lemma tfl_rev_eq_mp: "(x = y) --> y --> x"; |