changeset 39452 | 70a57e40f795 |
parent 39355 | 104a6d9e493e |
child 39494 | bf7dd4902321 |
--- a/src/HOL/Sledgehammer.thy Thu Sep 16 09:59:32 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Thu Sep 16 11:12:08 2010 +0200 @@ -11,6 +11,7 @@ imports Plain Hilbert_Choice uses ("Tools/ATP/atp_problem.ML") + ("Tools/ATP/atp_proof.ML") ("Tools/ATP/atp_systems.ML") ("~~/src/Tools/Metis/metis.ML") ("Tools/Sledgehammer/clausifier.ML") @@ -92,6 +93,7 @@ done use "Tools/ATP/atp_problem.ML" +use "Tools/ATP/atp_proof.ML" use "Tools/ATP/atp_systems.ML" setup ATP_Systems.setup