src/HOL/Sledgehammer.thy
changeset 37509 f39464d971c4
parent 37410 2bf7e6136047
child 37511 26afa11a1fb2
--- a/src/HOL/Sledgehammer.thy	Tue Jun 22 19:10:12 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Tue Jun 22 23:54:02 2010 +0200
@@ -17,6 +17,7 @@
   ("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
   ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
   ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
+  ("Tools/Sledgehammer/sledgehammer_tptp_format.ML")
   ("Tools/ATP_Manager/atp_manager.ML")
   ("Tools/ATP_Manager/atp_systems.ML")
   ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
@@ -103,6 +104,7 @@
 use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
 use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
 use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
+use "Tools/Sledgehammer/sledgehammer_tptp_format.ML"
 use "Tools/ATP_Manager/atp_manager.ML"
 use "Tools/ATP_Manager/atp_systems.ML"
 setup ATP_Systems.setup