author | smolkas |
Thu, 11 Jul 2013 20:08:06 +0200 | |
changeset 52592 | 8a25b17e3d79 |
parent 52555 | 6811291d1869 |
child 52611 | 831f7479c74f |
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 |
|
51178 | 14 |
|
48891 | 15 |
ML_file "Tools/Sledgehammer/async_manager.ML" |
16 |
ML_file "Tools/Sledgehammer/sledgehammer_util.ML" |
|
52555 | 17 |
ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML" |
48891 | 18 |
ML_file "Tools/Sledgehammer/sledgehammer_fact.ML" |
52555 | 19 |
ML_file "Tools/Sledgehammer/sledgehammer_reconstructor.ML" |
50264
a9ec48b98734
renamed sledgehammer_isar_reconstruct to sledgehammer_proof
smolkas
parents:
50259
diff
changeset
|
20 |
ML_file "Tools/Sledgehammer/sledgehammer_proof.ML" |
52555 | 21 |
ML_file "Tools/Sledgehammer/sledgehammer_print.ML" |
50923 | 22 |
ML_file "Tools/Sledgehammer/sledgehammer_preplay.ML" |
51130
76d68444cd59
renamed sledgehammer_shrink to sledgehammer_compress
smolkas
parents:
50923
diff
changeset
|
23 |
ML_file "Tools/Sledgehammer/sledgehammer_compress.ML" |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52555
diff
changeset
|
24 |
ML_file "Tools/Sledgehammer/sledgehammer_try0.ML" |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
25 |
ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML" |
48891 | 26 |
ML_file "Tools/Sledgehammer/sledgehammer_provers.ML" |
27 |
ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML" |
|
28 |
ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML" |
|
29 |
ML_file "Tools/Sledgehammer/sledgehammer_mash.ML" |
|
30 |
ML_file "Tools/Sledgehammer/sledgehammer_run.ML" |
|
31 |
ML_file "Tools/Sledgehammer/sledgehammer_isar.ML" |
|
32 |
||
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
41094
diff
changeset
|
33 |
setup {* Sledgehammer_Isar.setup *} |
23444 | 34 |
|
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
35 |
end |