--- a/src/HOL/Sledgehammer.thy Fri Jun 25 17:08:39 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Fri Jun 25 17:13:38 2010 +0200
@@ -18,9 +18,9 @@
("Tools/Sledgehammer/sledgehammer_util.ML")
("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
("Tools/Sledgehammer/sledgehammer_tptp_format.ML")
+ ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
("Tools/ATP_Manager/atp_manager.ML")
("Tools/ATP_Manager/atp_systems.ML")
- ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
("Tools/Sledgehammer/sledgehammer_isar.ML")
begin
@@ -96,10 +96,10 @@
use "Tools/Sledgehammer/sledgehammer_util.ML"
use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
use "Tools/Sledgehammer/sledgehammer_tptp_format.ML"
+use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
use "Tools/ATP_Manager/atp_manager.ML"
use "Tools/ATP_Manager/atp_systems.ML"
setup ATP_Systems.setup
-use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
use "Tools/Sledgehammer/sledgehammer_isar.ML"
setup Metis_Tactics.setup