src/HOL/ATP.thy
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 40178 00152d17855b
child 43085 0a2f5b86bdd7
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
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
blanchet@40178
     9
imports Plain
blanchet@40178
    10
uses "Tools/ATP/atp_problem.ML"
blanchet@40178
    11
     "Tools/ATP/atp_proof.ML"
blanchet@40178
    12
     "Tools/ATP/atp_systems.ML"
blanchet@39951
    13
begin
blanchet@39951
    14
blanchet@39951
    15
setup ATP_Systems.setup
blanchet@39951
    16
blanchet@39951
    17
end