equal
deleted
inserted
replaced
7 header {* Metis Proof Method *} |
7 header {* Metis Proof Method *} |
8 |
8 |
9 theory Metis |
9 theory Metis |
10 imports ATP |
10 imports ATP |
11 uses "~~/src/Tools/Metis/metis.ML" |
11 uses "~~/src/Tools/Metis/metis.ML" |
12 ("Tools/Metis/metis_translate.ML") |
12 ("Tools/Metis/metis_generate.ML") |
13 ("Tools/Metis/metis_reconstruct.ML") |
13 ("Tools/Metis/metis_reconstruct.ML") |
14 ("Tools/Metis/metis_tactic.ML") |
14 ("Tools/Metis/metis_tactic.ML") |
15 ("Tools/try_methods.ML") |
15 ("Tools/try_methods.ML") |
16 begin |
16 begin |
17 |
17 |
38 unfolding lambda_def by assumption |
38 unfolding lambda_def by assumption |
39 |
39 |
40 |
40 |
41 subsection {* Metis package *} |
41 subsection {* Metis package *} |
42 |
42 |
43 use "Tools/Metis/metis_translate.ML" |
43 use "Tools/Metis/metis_generate.ML" |
44 use "Tools/Metis/metis_reconstruct.ML" |
44 use "Tools/Metis/metis_reconstruct.ML" |
45 use "Tools/Metis/metis_tactic.ML" |
45 use "Tools/Metis/metis_tactic.ML" |
46 |
46 |
47 setup {* Metis_Tactic.setup *} |
47 setup {* Metis_Tactic.setup *} |
48 |
48 |