src/HOL/ATP.thy
changeset 45522 3b951bbd2bee
parent 44087 8e491cb8841c
child 45877 b18f62e40429
     1.1 --- a/src/HOL/ATP.thy	Wed Nov 16 17:06:14 2011 +0100
     1.2 +++ b/src/HOL/ATP.thy	Wed Nov 16 17:19:08 2011 +0100
     1.3 @@ -12,9 +12,9 @@
     1.4       "Tools/ATP/atp_util.ML"
     1.5       "Tools/ATP/atp_problem.ML"
     1.6       "Tools/ATP/atp_proof.ML"
     1.7 -     "Tools/ATP/atp_systems.ML"
     1.8       ("Tools/ATP/atp_translate.ML")
     1.9       ("Tools/ATP/atp_reconstruct.ML")
    1.10 +     ("Tools/ATP/atp_systems.ML")
    1.11  begin
    1.12  
    1.13  subsection {* Higher-order reasoning helpers *}
    1.14 @@ -50,6 +50,7 @@
    1.15  
    1.16  use "Tools/ATP/atp_translate.ML"
    1.17  use "Tools/ATP/atp_reconstruct.ML"
    1.18 +use "Tools/ATP/atp_systems.ML"
    1.19  
    1.20  setup ATP_Systems.setup
    1.21