Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more moving around of ML files in "Sledgehammer.thy"
authorblanchet
Fri, 25 Jun 2010 15:30:38 +0200
changeset 37571 76e23303c7ff
parent 37570 de5feddaa95c
child 37572 a899f9506f39
more moving around of ML files in "Sledgehammer.thy"
src/HOL/Sledgehammer.thy file | annotate | diff | comparison | revisions
src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Sledgehammer.thy	Fri Jun 25 15:22:12 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Fri Jun 25 15:30:38 2010 +0200
@@ -11,16 +11,16 @@
 imports Plain Hilbert_Choice
 uses
   "~~/src/Tools/Metis/metis.ML"
-  "Tools/Sledgehammer/sledgehammer_util.ML"
-  ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
   ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
   ("Tools/Sledgehammer/meson_tactic.ML")
+  ("Tools/Sledgehammer/sledgehammer_util.ML")
+  ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
   ("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_proof_reconstruct.ML")
   ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
   ("Tools/Sledgehammer/sledgehammer_isar.ML")
   ("Tools/Sledgehammer/metis_tactics.ML")
@@ -85,19 +85,20 @@
 apply (simp add: COMBC_def) 
 done
 
-
-use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
 use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML"
 setup Sledgehammer_Fact_Preprocessor.setup
 use "Tools/Sledgehammer/meson_tactic.ML"
 setup Meson_Tactic.setup
+
+use "Tools/Sledgehammer/sledgehammer_util.ML"
+use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
 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
+use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
 use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
 use "Tools/Sledgehammer/sledgehammer_isar.ML"
 use "Tools/Sledgehammer/metis_tactics.ML"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri Jun 25 15:22:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri Jun 25 15:30:38 2010 +0200
@@ -35,8 +35,6 @@
 structure Sledgehammer_Fact_Preprocessor : SLEDGEHAMMER_FACT_PREPROCESSOR =
 struct
 
-open Sledgehammer_FOL_Clause
-
 type cnf_thm = thm * ((string * int) * thm)
 
 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
isabelle