equal
deleted
inserted
replaced
13 ("../TFL/thms.ML") |
13 ("../TFL/thms.ML") |
14 ("../TFL/rules.ML") |
14 ("../TFL/rules.ML") |
15 ("../TFL/thry.ML") |
15 ("../TFL/thry.ML") |
16 ("../TFL/tfl.ML") |
16 ("../TFL/tfl.ML") |
17 ("../TFL/post.ML") |
17 ("../TFL/post.ML") |
18 ("Tools/recdef_package.ML"): |
18 ("Tools/recdef_package.ML") |
|
19 ("Tools/basic_codegen.ML") |
|
20 ("Tools/inductive_codegen.ML"): |
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"; |
48 use "../TFL/rules.ML" |
50 use "../TFL/rules.ML" |
49 use "../TFL/thry.ML" |
51 use "../TFL/thry.ML" |
50 use "../TFL/tfl.ML" |
52 use "../TFL/tfl.ML" |
51 use "../TFL/post.ML" |
53 use "../TFL/post.ML" |
52 use "Tools/recdef_package.ML" |
54 use "Tools/recdef_package.ML" |
|
55 use "Tools/basic_codegen.ML" |
|
56 use "Tools/inductive_codegen.ML" |
53 setup RecdefPackage.setup |
57 setup RecdefPackage.setup |
|
58 setup BasicCodegen.setup |
|
59 setup InductiveCodegen.setup |
54 |
60 |
55 lemmas [recdef_simp] = |
61 lemmas [recdef_simp] = |
56 inv_image_def |
62 inv_image_def |
57 measure_def |
63 measure_def |
58 lex_prod_def |
64 lex_prod_def |