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 keywords "try0" :: diag |
11 keywords "try0" :: diag |
12 uses "~~/src/Tools/Metis/metis.ML" |
|
13 ("Tools/Metis/metis_generate.ML") |
|
14 ("Tools/Metis/metis_reconstruct.ML") |
|
15 ("Tools/Metis/metis_tactic.ML") |
|
16 ("Tools/try0.ML") |
|
17 begin |
12 begin |
|
13 |
|
14 ML_file "~~/src/Tools/Metis/metis.ML" |
18 |
15 |
19 subsection {* Literal selection and lambda-lifting helpers *} |
16 subsection {* Literal selection and lambda-lifting helpers *} |
20 |
17 |
21 definition select :: "'a \<Rightarrow> 'a" where |
18 definition select :: "'a \<Rightarrow> 'a" where |
22 [no_atp]: "select = (\<lambda>x. x)" |
19 [no_atp]: "select = (\<lambda>x. x)" |
39 unfolding lambda_def by assumption |
36 unfolding lambda_def by assumption |
40 |
37 |
41 |
38 |
42 subsection {* Metis package *} |
39 subsection {* Metis package *} |
43 |
40 |
44 use "Tools/Metis/metis_generate.ML" |
41 ML_file "Tools/Metis/metis_generate.ML" |
45 use "Tools/Metis/metis_reconstruct.ML" |
42 ML_file "Tools/Metis/metis_reconstruct.ML" |
46 use "Tools/Metis/metis_tactic.ML" |
43 ML_file "Tools/Metis/metis_tactic.ML" |
47 |
44 |
48 setup {* Metis_Tactic.setup *} |
45 setup {* Metis_Tactic.setup *} |
49 |
46 |
50 hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fequal |
47 hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fequal |
51 lambda |
48 lambda |
56 fimplies_laws fequal_laws fAll_law fEx_law lambda_def eq_lambdaI |
53 fimplies_laws fequal_laws fAll_law fEx_law lambda_def eq_lambdaI |
57 |
54 |
58 |
55 |
59 subsection {* Try0 *} |
56 subsection {* Try0 *} |
60 |
57 |
61 use "Tools/try0.ML" |
58 ML_file "Tools/try0.ML" |
62 |
|
63 setup {* Try0.setup *} |
59 setup {* Try0.setup *} |
64 |
60 |
65 end |
61 end |