src/HOL/Sledgehammer.thy
changeset 49395 d4b7c7be3116
parent 49303 255c6e1fd505
child 49906 c0eafbd55de3
equal deleted inserted replaced
49394:2b5ad61e2ccc 49395:d4b7c7be3116
    12 uses "Tools/Sledgehammer/async_manager.ML"
    12 uses "Tools/Sledgehammer/async_manager.ML"
    13      "Tools/Sledgehammer/sledgehammer_util.ML"
    13      "Tools/Sledgehammer/sledgehammer_util.ML"
    14      "Tools/Sledgehammer/sledgehammer_fact.ML"
    14      "Tools/Sledgehammer/sledgehammer_fact.ML"
    15      "Tools/Sledgehammer/sledgehammer_provers.ML"
    15      "Tools/Sledgehammer/sledgehammer_provers.ML"
    16      "Tools/Sledgehammer/sledgehammer_minimize.ML"
    16      "Tools/Sledgehammer/sledgehammer_minimize.ML"
    17      "Tools/Sledgehammer/sledgehammer_filter_iter.ML"
    17      "Tools/Sledgehammer/sledgehammer_mepo.ML"
    18      "Tools/Sledgehammer/sledgehammer_filter_mash.ML"
    18      "Tools/Sledgehammer/sledgehammer_mash.ML"
    19      "Tools/Sledgehammer/sledgehammer_run.ML"
    19      "Tools/Sledgehammer/sledgehammer_run.ML"
    20      "Tools/Sledgehammer/sledgehammer_isar.ML"
    20      "Tools/Sledgehammer/sledgehammer_isar.ML"
    21 begin
    21 begin
    22 
    22 
    23 setup {* Sledgehammer_Isar.setup *}
    23 setup {* Sledgehammer_Isar.setup *}