equal
deleted
inserted
replaced
14 ("Tools/TFL/thms.ML") |
14 ("Tools/TFL/thms.ML") |
15 ("Tools/TFL/rules.ML") |
15 ("Tools/TFL/rules.ML") |
16 ("Tools/TFL/thry.ML") |
16 ("Tools/TFL/thry.ML") |
17 ("Tools/TFL/tfl.ML") |
17 ("Tools/TFL/tfl.ML") |
18 ("Tools/TFL/post.ML") |
18 ("Tools/TFL/post.ML") |
19 ("Tools/recdef_package.ML") |
19 ("Tools/recdef.ML") |
20 begin |
20 begin |
21 |
21 |
22 text{** This form avoids giant explosions in proofs. NOTE USE OF ==*} |
22 text{** This form avoids giant explosions in proofs. NOTE USE OF ==*} |
23 lemma def_wfrec: "[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a" |
23 lemma def_wfrec: "[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a" |
24 apply auto |
24 apply auto |
74 use "Tools/TFL/thms.ML" |
74 use "Tools/TFL/thms.ML" |
75 use "Tools/TFL/rules.ML" |
75 use "Tools/TFL/rules.ML" |
76 use "Tools/TFL/thry.ML" |
76 use "Tools/TFL/thry.ML" |
77 use "Tools/TFL/tfl.ML" |
77 use "Tools/TFL/tfl.ML" |
78 use "Tools/TFL/post.ML" |
78 use "Tools/TFL/post.ML" |
79 use "Tools/recdef_package.ML" |
79 use "Tools/recdef.ML" |
80 setup RecdefPackage.setup |
80 setup Recdef.setup |
81 |
81 |
82 lemmas [recdef_simp] = |
82 lemmas [recdef_simp] = |
83 inv_image_def |
83 inv_image_def |
84 measure_def |
84 measure_def |
85 lex_prod_def |
85 lex_prod_def |