src/HOL/Sledgehammer.thy
author blanchet
Mon Oct 04 22:45:09 2010 +0200 (2010-10-04)
changeset 39946 78faa9b31202
parent 39942 1ae333bfef14
child 39947 f95834c8bb4d
permissions -rw-r--r--
move Metis into Plain
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
wenzelm@21254
    12
uses
blanchet@38047
    13
  ("Tools/ATP/atp_problem.ML")
blanchet@39452
    14
  ("Tools/ATP/atp_proof.ML")
blanchet@38047
    15
  ("Tools/ATP/atp_systems.ML")
blanchet@37571
    16
  ("Tools/Sledgehammer/sledgehammer_util.ML")
blanchet@38988
    17
  ("Tools/Sledgehammer/sledgehammer_filter.ML")
blanchet@38282
    18
  ("Tools/Sledgehammer/sledgehammer_translate.ML")
blanchet@38988
    19
  ("Tools/Sledgehammer/sledgehammer_reconstruct.ML")
blanchet@38023
    20
  ("Tools/Sledgehammer/sledgehammer.ML")
blanchet@38988
    21
  ("Tools/Sledgehammer/sledgehammer_minimize.ML")
blanchet@35866
    22
  ("Tools/Sledgehammer/sledgehammer_isar.ML")
wenzelm@21254
    23
begin
wenzelm@21254
    24
blanchet@38047
    25
use "Tools/ATP/atp_problem.ML"
blanchet@39452
    26
use "Tools/ATP/atp_proof.ML"
blanchet@38047
    27
use "Tools/ATP/atp_systems.ML"
blanchet@38025
    28
setup ATP_Systems.setup
blanchet@38025
    29
blanchet@37571
    30
use "Tools/Sledgehammer/sledgehammer_util.ML"
blanchet@38988
    31
use "Tools/Sledgehammer/sledgehammer_filter.ML"
blanchet@38282
    32
use "Tools/Sledgehammer/sledgehammer_translate.ML"
blanchet@38988
    33
use "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
blanchet@38023
    34
use "Tools/Sledgehammer/sledgehammer.ML"
blanchet@38023
    35
setup Sledgehammer.setup
blanchet@38988
    36
use "Tools/Sledgehammer/sledgehammer_minimize.ML"
blanchet@35866
    37
use "Tools/Sledgehammer/sledgehammer_isar.ML"
blanchet@39322
    38
setup Sledgehammer_Isar.setup
wenzelm@23444
    39
wenzelm@21254
    40
end