--- 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