author | bulwahn |
Wed, 08 Dec 2010 18:07:03 +0100 | |
changeset 41085 | a549ff1d4070 |
parent 41042 | 8275f52ac991 |
child 41087 | d7b5fd465198 |
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 |
41042
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
40181
diff
changeset
|
11 |
uses "Tools/Sledgehammer/async_manager.ML" |
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
40181
diff
changeset
|
12 |
"Tools/Sledgehammer/sledgehammer_util.ML" |
39947 | 13 |
"Tools/Sledgehammer/sledgehammer_filter.ML" |
40067 | 14 |
"Tools/Sledgehammer/sledgehammer_atp_translate.ML" |
15 |
"Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML" |
|
39947 | 16 |
"Tools/Sledgehammer/sledgehammer.ML" |
17 |
"Tools/Sledgehammer/sledgehammer_minimize.ML" |
|
18 |
"Tools/Sledgehammer/sledgehammer_isar.ML" |
|
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
19 |
begin |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
20 |
|
39947 | 21 |
setup {* |
39951
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
39947
diff
changeset
|
22 |
Sledgehammer.setup |
39947 | 23 |
#> Sledgehammer_Isar.setup |
24 |
*} |
|
23444 | 25 |
|
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
26 |
end |