src/HOL/Sledgehammer.thy
changeset 38988 483879af0643
parent 38606 3003ddbd46d9
child 38990 7fba3ccc755a
     1.1 --- a/src/HOL/Sledgehammer.thy	Tue Aug 31 23:50:40 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Tue Aug 31 23:50:59 2010 +0200
     1.3 @@ -19,11 +19,11 @@
     1.4    ("Tools/Sledgehammer/metis_clauses.ML")
     1.5    ("Tools/Sledgehammer/metis_tactics.ML")
     1.6    ("Tools/Sledgehammer/sledgehammer_util.ML")
     1.7 -  ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
     1.8 +  ("Tools/Sledgehammer/sledgehammer_filter.ML")
     1.9    ("Tools/Sledgehammer/sledgehammer_translate.ML")
    1.10 -  ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
    1.11 +  ("Tools/Sledgehammer/sledgehammer_reconstruct.ML")
    1.12    ("Tools/Sledgehammer/sledgehammer.ML")
    1.13 -  ("Tools/Sledgehammer/sledgehammer_fact_minimize.ML")
    1.14 +  ("Tools/Sledgehammer/sledgehammer_minimize.ML")
    1.15    ("Tools/Sledgehammer/sledgehammer_isar.ML")
    1.16  begin
    1.17  
    1.18 @@ -103,12 +103,12 @@
    1.19  use "Tools/Sledgehammer/metis_tactics.ML"
    1.20  
    1.21  use "Tools/Sledgehammer/sledgehammer_util.ML"
    1.22 -use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
    1.23 +use "Tools/Sledgehammer/sledgehammer_filter.ML"
    1.24  use "Tools/Sledgehammer/sledgehammer_translate.ML"
    1.25 -use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
    1.26 +use "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
    1.27  use "Tools/Sledgehammer/sledgehammer.ML"
    1.28  setup Sledgehammer.setup
    1.29 -use "Tools/Sledgehammer/sledgehammer_fact_minimize.ML"
    1.30 +use "Tools/Sledgehammer/sledgehammer_minimize.ML"
    1.31  use "Tools/Sledgehammer/sledgehammer_isar.ML"
    1.32  setup Metis_Tactics.setup
    1.33