src/HOL/Sledgehammer.thy
changeset 37578 9367cb36b1c4
parent 37577 5379f41a1322
child 37579 61a01843a028
     1.1 --- a/src/HOL/Sledgehammer.thy	Fri Jun 25 16:42:06 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Fri Jun 25 17:08:39 2010 +0200
     1.3 @@ -13,8 +13,9 @@
     1.4    "~~/src/Tools/Metis/metis.ML"
     1.5    ("Tools/Sledgehammer/clausifier.ML")
     1.6    ("Tools/Sledgehammer/meson_tactic.ML")
     1.7 +  ("Tools/Sledgehammer/metis_clauses.ML")
     1.8 +  ("Tools/Sledgehammer/metis_tactics.ML")
     1.9    ("Tools/Sledgehammer/sledgehammer_util.ML")
    1.10 -  ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
    1.11    ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
    1.12    ("Tools/Sledgehammer/sledgehammer_tptp_format.ML")
    1.13    ("Tools/ATP_Manager/atp_manager.ML")
    1.14 @@ -22,7 +23,6 @@
    1.15    ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
    1.16    ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
    1.17    ("Tools/Sledgehammer/sledgehammer_isar.ML")
    1.18 -  ("Tools/Sledgehammer/metis_tactics.ML")
    1.19  begin
    1.20  
    1.21  definition skolem_id :: "'a \<Rightarrow> 'a" where
    1.22 @@ -86,11 +86,14 @@
    1.23  
    1.24  use "Tools/Sledgehammer/clausifier.ML"
    1.25  setup Clausifier.setup
    1.26 +
    1.27  use "Tools/Sledgehammer/meson_tactic.ML"
    1.28  setup Meson_Tactic.setup
    1.29  
    1.30 +use "Tools/Sledgehammer/metis_clauses.ML"
    1.31 +use "Tools/Sledgehammer/metis_tactics.ML"
    1.32 +
    1.33  use "Tools/Sledgehammer/sledgehammer_util.ML"
    1.34 -use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
    1.35  use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
    1.36  use "Tools/Sledgehammer/sledgehammer_tptp_format.ML"
    1.37  use "Tools/ATP_Manager/atp_manager.ML"
    1.38 @@ -99,7 +102,6 @@
    1.39  use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
    1.40  use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
    1.41  use "Tools/Sledgehammer/sledgehammer_isar.ML"
    1.42 -use "Tools/Sledgehammer/metis_tactics.ML"
    1.43  setup Metis_Tactics.setup
    1.44  
    1.45  end