author | smolkas |
Thu, 14 Feb 2013 22:49:22 +0100 | |
changeset 51130 | 76d68444cd59 |
parent 50923 | 141d8f575f6f |
child 51178 | 06689dbfe072 |
permissions | -rw-r--r-- |
35827 | 1 |
(* Title: HOL/Sledgehammer.thy |
38027 | 2 |
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory |
38028 | 3 |
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA |
35865 | 4 |
Author: Jasmin Blanchette, TU Muenchen |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
5 |
*) |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
6 |
|
35827 | 7 |
header {* Sledgehammer: Isabelle--ATP Linkup *} |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
8 |
|
35827 | 9 |
theory Sledgehammer |
40181 | 10 |
imports ATP SMT |
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
43085
diff
changeset
|
11 |
keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
12 |
begin |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
13 |
|
48891 | 14 |
ML_file "Tools/Sledgehammer/async_manager.ML" |
15 |
ML_file "Tools/Sledgehammer/sledgehammer_util.ML" |
|
16 |
ML_file "Tools/Sledgehammer/sledgehammer_fact.ML" |
|
50264
a9ec48b98734
renamed sledgehammer_isar_reconstruct to sledgehammer_proof
smolkas
parents:
50259
diff
changeset
|
17 |
ML_file "Tools/Sledgehammer/sledgehammer_proof.ML" |
50258 | 18 |
ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML" |
50923 | 19 |
ML_file "Tools/Sledgehammer/sledgehammer_preplay.ML" |
51130
76d68444cd59
renamed sledgehammer_shrink to sledgehammer_compress
smolkas
parents:
50923
diff
changeset
|
20 |
ML_file "Tools/Sledgehammer/sledgehammer_compress.ML" |
49881
d9d73ebf9274
added proof minimization code from Steffen Smolka
blanchet
parents:
48891
diff
changeset
|
21 |
ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML" |
48891 | 22 |
ML_file "Tools/Sledgehammer/sledgehammer_provers.ML" |
23 |
ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML" |
|
24 |
ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML" |
|
25 |
ML_file "Tools/Sledgehammer/sledgehammer_mash.ML" |
|
26 |
ML_file "Tools/Sledgehammer/sledgehammer_run.ML" |
|
27 |
ML_file "Tools/Sledgehammer/sledgehammer_isar.ML" |
|
28 |
||
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
41094
diff
changeset
|
29 |
setup {* Sledgehammer_Isar.setup *} |
23444 | 30 |
|
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
31 |
end |