src/HOL/Sledgehammer.thy
author wenzelm
Mon, 02 May 2011 16:33:21 +0200
changeset 42616 92715b528e78
parent 41094 1dc7652ce404
child 43085 0a2f5b86bdd7
permissions -rw-r--r--
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35827
f552152d7747 renamed "ATP_Linkup" theory to "Sledgehammer"
blanchet
parents: 35826
diff changeset
     1
(*  Title:      HOL/Sledgehammer.thy
38027
505657ddb047 standardize "Author" tags
blanchet
parents: 38025
diff changeset
     2
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
     3
    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35827
diff changeset
     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
f552152d7747 renamed "ATP_Linkup" theory to "Sledgehammer"
blanchet
parents: 35826
diff changeset
     7
header {* Sledgehammer: Isabelle--ATP Linkup *}
21254
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
     8
35827
f552152d7747 renamed "ATP_Linkup" theory to "Sledgehammer"
blanchet
parents: 35826
diff changeset
     9
theory Sledgehammer
40181
3788b7adab36 integrated "smt" proof method with Sledgehammer
blanchet
parents: 40178
diff changeset
    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
blanchet
parents: 39946
diff changeset
    13
     "Tools/Sledgehammer/sledgehammer_filter.ML"
40067
0783415ed7f0 renamed files
blanchet
parents: 39951
diff changeset
    14
     "Tools/Sledgehammer/sledgehammer_atp_translate.ML"
0783415ed7f0 renamed files
blanchet
parents: 39951
diff changeset
    15
     "Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML"
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41042
diff changeset
    16
     "Tools/Sledgehammer/sledgehammer_provers.ML"
39947
blanchet
parents: 39946
diff changeset
    17
     "Tools/Sledgehammer/sledgehammer_minimize.ML"
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41042
diff changeset
    18
     "Tools/Sledgehammer/sledgehammer_run.ML"
39947
blanchet
parents: 39946
diff changeset
    19
     "Tools/Sledgehammer/sledgehammer_isar.ML"
21254
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    20
begin
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    21
42616
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 41094
diff changeset
    22
setup {* Sledgehammer_Isar.setup *}
23444
6d4703843f93 added Metis setup (from Metis.thy);
wenzelm
parents: 21999
diff changeset
    23
21254
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    24
end