src/HOL/Sledgehammer.thy
changeset 38990 7fba3ccc755a
parent 38988 483879af0643
child 39036 dff91b90d74c
     1.1 --- a/src/HOL/Sledgehammer.thy	Tue Aug 31 23:52:59 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Wed Sep 01 00:03:15 2010 +0200
     1.3 @@ -10,7 +10,6 @@
     1.4  theory Sledgehammer
     1.5  imports Plain Hilbert_Choice
     1.6  uses
     1.7 -  ("Tools/ATP/async_manager.ML")
     1.8    ("Tools/ATP/atp_problem.ML")
     1.9    ("Tools/ATP/atp_systems.ML")
    1.10    ("~~/src/Tools/Metis/metis.ML")
    1.11 @@ -89,7 +88,6 @@
    1.12  apply (simp add: COMBC_def) 
    1.13  done
    1.14  
    1.15 -use "Tools/ATP/async_manager.ML"
    1.16  use "Tools/ATP/atp_problem.ML"
    1.17  use "Tools/ATP/atp_systems.ML"
    1.18  setup ATP_Systems.setup