src/HOL/Sledgehammer.thy
author blanchet
Mon Oct 04 22:51:53 2010 +0200 (2010-10-04)
changeset 39947 f95834c8bb4d
parent 39946 78faa9b31202
child 39951 ff60a6e4edfe
permissions -rw-r--r--
tuning
blanchet@35827
     1
(*  Title:      HOL/Sledgehammer.thy
blanchet@38027
     2
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
blanchet@38028
     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@39946
    11
imports Plain
blanchet@39947
    12
uses "Tools/ATP/atp_problem.ML"
blanchet@39947
    13
     "Tools/ATP/atp_proof.ML"
blanchet@39947
    14
     "Tools/ATP/atp_systems.ML"
blanchet@39947
    15
     "Tools/Sledgehammer/sledgehammer_util.ML"
blanchet@39947
    16
     "Tools/Sledgehammer/sledgehammer_filter.ML"
blanchet@39947
    17
     "Tools/Sledgehammer/sledgehammer_translate.ML"
blanchet@39947
    18
     "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
blanchet@39947
    19
     "Tools/Sledgehammer/sledgehammer.ML"
blanchet@39947
    20
     "Tools/Sledgehammer/sledgehammer_minimize.ML"
blanchet@39947
    21
     "Tools/Sledgehammer/sledgehammer_isar.ML"
wenzelm@21254
    22
begin
wenzelm@21254
    23
blanchet@39947
    24
setup {*
blanchet@39947
    25
  ATP_Systems.setup
blanchet@39947
    26
  #> Sledgehammer.setup
blanchet@39947
    27
  #> Sledgehammer_Isar.setup
blanchet@39947
    28
*}
wenzelm@23444
    29
wenzelm@21254
    30
end