src/HOL/Sledgehammer.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46950 d0181abdbdac
child 48250 1065c307fafe
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
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
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
41042
8275f52ac991 load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents: 40181
diff changeset
    12
uses "Tools/Sledgehammer/async_manager.ML"
8275f52ac991 load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents: 40181
diff changeset
    13
     "Tools/Sledgehammer/sledgehammer_util.ML"
39947
blanchet
parents: 39946
diff changeset
    14
     "Tools/Sledgehammer/sledgehammer_filter.ML"
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41042
diff changeset
    15
     "Tools/Sledgehammer/sledgehammer_provers.ML"
39947
blanchet
parents: 39946
diff changeset
    16
     "Tools/Sledgehammer/sledgehammer_minimize.ML"
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41042
diff changeset
    17
     "Tools/Sledgehammer/sledgehammer_run.ML"
39947
blanchet
parents: 39946
diff changeset
    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
42616
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 41094
diff changeset
    21
setup {* Sledgehammer_Isar.setup *}
23444
6d4703843f93 added Metis setup (from Metis.thy);
wenzelm
parents: 21999
diff changeset
    22
21254
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    23
end