src/HOL/ATP.thy
author haftmann
Mon Oct 25 13:34:57 2010 +0200 (2010-10-25)
changeset 40121 e7a80c6752c9
parent 39958 88c9aa5666de
child 40178 00152d17855b
permissions -rw-r--r--
moved sledgehammer to Plain; tuned dependencies
blanchet@39951
     1
(*  Title:      HOL/ATP.thy
blanchet@39951
     2
    Author:     Fabian Immler, TU Muenchen
blanchet@39951
     3
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@39951
     4
*)
blanchet@39951
     5
blanchet@39958
     6
header {* Automatic Theorem Provers (ATPs) *}
blanchet@39951
     7
blanchet@39951
     8
theory ATP
haftmann@40121
     9
imports HOL
haftmann@40121
    10
uses
haftmann@40121
    11
  "Tools/ATP/atp_problem.ML"
haftmann@40121
    12
  "Tools/ATP/atp_proof.ML"
haftmann@40121
    13
  "Tools/ATP/atp_systems.ML"
blanchet@39951
    14
begin
blanchet@39951
    15
blanchet@39951
    16
setup ATP_Systems.setup
blanchet@39951
    17
blanchet@39951
    18
end