src/HOL/Sledgehammer.thy
changeset 39452 70a57e40f795
parent 39355 104a6d9e493e
child 39494 bf7dd4902321
     1.1 --- a/src/HOL/Sledgehammer.thy	Thu Sep 16 09:59:32 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Thu Sep 16 11:12:08 2010 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4  imports Plain Hilbert_Choice
     1.5  uses
     1.6    ("Tools/ATP/atp_problem.ML")
     1.7 +  ("Tools/ATP/atp_proof.ML")
     1.8    ("Tools/ATP/atp_systems.ML")
     1.9    ("~~/src/Tools/Metis/metis.ML")
    1.10    ("Tools/Sledgehammer/clausifier.ML")
    1.11 @@ -92,6 +93,7 @@
    1.12  done
    1.13  
    1.14  use "Tools/ATP/atp_problem.ML"
    1.15 +use "Tools/ATP/atp_proof.ML"
    1.16  use "Tools/ATP/atp_systems.ML"
    1.17  setup ATP_Systems.setup
    1.18