src/HOL/ATP.thy
changeset 40178 00152d17855b
parent 40121 e7a80c6752c9
child 43085 0a2f5b86bdd7
     1.1 --- a/src/HOL/ATP.thy	Tue Oct 26 11:51:09 2010 +0200
     1.2 +++ b/src/HOL/ATP.thy	Tue Oct 26 12:17:19 2010 +0200
     1.3 @@ -6,11 +6,10 @@
     1.4  header {* Automatic Theorem Provers (ATPs) *}
     1.5  
     1.6  theory ATP
     1.7 -imports HOL
     1.8 -uses
     1.9 -  "Tools/ATP/atp_problem.ML"
    1.10 -  "Tools/ATP/atp_proof.ML"
    1.11 -  "Tools/ATP/atp_systems.ML"
    1.12 +imports Plain
    1.13 +uses "Tools/ATP/atp_problem.ML"
    1.14 +     "Tools/ATP/atp_proof.ML"
    1.15 +     "Tools/ATP/atp_systems.ML"
    1.16  begin
    1.17  
    1.18  setup ATP_Systems.setup