src/HOL/Sledgehammer.thy
changeset 37574 b8c1f4c46983
parent 37571 76e23303c7ff
child 37577 5379f41a1322
     1.1 --- a/src/HOL/Sledgehammer.thy	Fri Jun 25 16:03:34 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Fri Jun 25 16:15:03 2010 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  imports Plain Hilbert_Choice
     1.5  uses
     1.6    "~~/src/Tools/Metis/metis.ML"
     1.7 -  ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
     1.8 +  ("Tools/Sledgehammer/clausifier.ML")
     1.9    ("Tools/Sledgehammer/meson_tactic.ML")
    1.10    ("Tools/Sledgehammer/sledgehammer_util.ML")
    1.11    ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
    1.12 @@ -85,8 +85,8 @@
    1.13  apply (simp add: COMBC_def) 
    1.14  done
    1.15  
    1.16 -use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML"
    1.17 -setup Sledgehammer_Fact_Preprocessor.setup
    1.18 +use "Tools/Sledgehammer/clausifier.ML"
    1.19 +setup Clausifier.setup
    1.20  use "Tools/Sledgehammer/meson_tactic.ML"
    1.21  setup Meson_Tactic.setup
    1.22