src/HOL/Sledgehammer.thy
changeset 39494 bf7dd4902321
parent 39452 70a57e40f795
child 39495 bb4fb9ffe2d1
     1.1 --- a/src/HOL/Sledgehammer.thy	Thu Sep 16 15:38:46 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Thu Sep 16 16:12:02 2010 +0200
     1.3 @@ -16,7 +16,7 @@
     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_translate.ML")
     1.9    ("Tools/Sledgehammer/metis_tactics.ML")
    1.10    ("Tools/Sledgehammer/sledgehammer_util.ML")
    1.11    ("Tools/Sledgehammer/sledgehammer_filter.ML")
    1.12 @@ -102,7 +102,7 @@
    1.13  use "Tools/Sledgehammer/meson_tactic.ML"
    1.14  setup Meson_Tactic.setup
    1.15  
    1.16 -use "Tools/Sledgehammer/metis_clauses.ML"
    1.17 +use "Tools/Sledgehammer/metis_translate.ML"
    1.18  use "Tools/Sledgehammer/metis_tactics.ML"
    1.19  setup Metis_Tactics.setup
    1.20