author | blanchet |
Wed, 11 Jul 2012 21:43:19 +0200 | |
changeset 49265 | 1065c307fafe |
parent 47824 | d0181abdbdac |
child 49266 | 6cdcfbddc077 |
permissions | -rw-r--r-- |
blanchet@35827 | 1 |
(* Title: HOL/Sledgehammer.thy |
blanchet@38261 | 2 |
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory |
blanchet@38262 | 3 |
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA |
blanchet@35865 | 4 |
Author: Jasmin Blanchette, TU Muenchen |
wenzelm@21254 | 5 |
*) |
wenzelm@21254 | 6 |
|
blanchet@35827 | 7 |
header {* Sledgehammer: Isabelle--ATP Linkup *} |
wenzelm@21254 | 8 |
|
blanchet@35827 | 9 |
theory Sledgehammer |
blanchet@40422 | 10 |
imports ATP SMT |
wenzelm@47824 | 11 |
keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl |
blanchet@41290 | 12 |
uses "Tools/Sledgehammer/async_manager.ML" |
blanchet@41290 | 13 |
"Tools/Sledgehammer/sledgehammer_util.ML" |
blanchet@49265 | 14 |
"Tools/Sledgehammer/sledgehammer_fact.ML" |
blanchet@49265 | 15 |
"Tools/Sledgehammer/sledgehammer_filter_iter.ML" |
blanchet@49265 | 16 |
"Tools/Sledgehammer/sledgehammer_provers.ML" |
blanchet@49265 | 17 |
"Tools/Sledgehammer/sledgehammer_filter_mash.ML" |
blanchet@40128 | 18 |
"Tools/Sledgehammer/sledgehammer_filter.ML" |
blanchet@40128 | 19 |
"Tools/Sledgehammer/sledgehammer_minimize.ML" |
blanchet@41335 | 20 |
"Tools/Sledgehammer/sledgehammer_run.ML" |
blanchet@40128 | 21 |
"Tools/Sledgehammer/sledgehammer_isar.ML" |
wenzelm@21254 | 22 |
begin |
wenzelm@21254 | 23 |
|
wenzelm@43487 | 24 |
setup {* Sledgehammer_Isar.setup *} |
wenzelm@23444 | 25 |
|
wenzelm@21254 | 26 |
end |