| author | blanchet |
| Mon, 04 Oct 2010 22:51:53 +0200 | |
| changeset 40128 | f95834c8bb4d |
| parent 40127 | 78faa9b31202 |
| child 40132 | ff60a6e4edfe |
| 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: Fabian Immler, TU Muenchen |
| blanchet@35865 | 5 |
Author: Jasmin Blanchette, TU Muenchen |
| wenzelm@21254 | 6 |
*) |
| wenzelm@21254 | 7 |
|
| blanchet@35827 | 8 |
header {* Sledgehammer: Isabelle--ATP Linkup *}
|
| wenzelm@21254 | 9 |
|
| blanchet@35827 | 10 |
theory Sledgehammer |
| blanchet@40127 | 11 |
imports Plain |
| blanchet@40128 | 12 |
uses "Tools/ATP/atp_problem.ML" |
| blanchet@40128 | 13 |
"Tools/ATP/atp_proof.ML" |
| blanchet@40128 | 14 |
"Tools/ATP/atp_systems.ML" |
| blanchet@40128 | 15 |
"Tools/Sledgehammer/sledgehammer_util.ML" |
| blanchet@40128 | 16 |
"Tools/Sledgehammer/sledgehammer_filter.ML" |
| blanchet@40128 | 17 |
"Tools/Sledgehammer/sledgehammer_translate.ML" |
| blanchet@40128 | 18 |
"Tools/Sledgehammer/sledgehammer_reconstruct.ML" |
| blanchet@40128 | 19 |
"Tools/Sledgehammer/sledgehammer.ML" |
| blanchet@40128 | 20 |
"Tools/Sledgehammer/sledgehammer_minimize.ML" |
| blanchet@40128 | 21 |
"Tools/Sledgehammer/sledgehammer_isar.ML" |
| wenzelm@21254 | 22 |
begin |
| wenzelm@21254 | 23 |
|
| blanchet@40128 | 24 |
setup {*
|
| blanchet@40128 | 25 |
ATP_Systems.setup |
| blanchet@40128 | 26 |
#> Sledgehammer.setup |
| blanchet@40128 | 27 |
#> Sledgehammer_Isar.setup |
| blanchet@40128 | 28 |
*} |
| wenzelm@23444 | 29 |
|
| wenzelm@21254 | 30 |
end |