src/HOL/Sledgehammer.thy
changeset 48288 255c6e1fd505
parent 48251 6cdcfbddc077
child 48380 d4b7c7be3116
     1.1 --- a/src/HOL/Sledgehammer.thy	Wed Jul 18 08:44:03 2012 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Wed Jul 18 08:44:03 2012 +0200
     1.3 @@ -12,11 +12,10 @@
     1.4  uses "Tools/Sledgehammer/async_manager.ML"
     1.5       "Tools/Sledgehammer/sledgehammer_util.ML"
     1.6       "Tools/Sledgehammer/sledgehammer_fact.ML"
     1.7 -     "Tools/Sledgehammer/sledgehammer_filter_iter.ML"
     1.8       "Tools/Sledgehammer/sledgehammer_provers.ML"
     1.9       "Tools/Sledgehammer/sledgehammer_minimize.ML"
    1.10 +     "Tools/Sledgehammer/sledgehammer_filter_iter.ML"
    1.11       "Tools/Sledgehammer/sledgehammer_filter_mash.ML"
    1.12 -     "Tools/Sledgehammer/sledgehammer_filter.ML"
    1.13       "Tools/Sledgehammer/sledgehammer_run.ML"
    1.14       "Tools/Sledgehammer/sledgehammer_isar.ML"
    1.15  begin