src/HOL/ATP.thy
changeset 40121 e7a80c6752c9
parent 39958 88c9aa5666de
child 40178 00152d17855b
     1.1 --- a/src/HOL/ATP.thy	Mon Oct 25 13:34:57 2010 +0200
     1.2 +++ b/src/HOL/ATP.thy	Mon Oct 25 13:34:57 2010 +0200
     1.3 @@ -6,10 +6,11 @@
     1.4  header {* Automatic Theorem Provers (ATPs) *}
     1.5  
     1.6  theory ATP
     1.7 -imports Plain
     1.8 -uses "Tools/ATP/atp_problem.ML"
     1.9 -     "Tools/ATP/atp_proof.ML"
    1.10 -     "Tools/ATP/atp_systems.ML"
    1.11 +imports HOL
    1.12 +uses
    1.13 +  "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