1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:03 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:03 2012 +0200
     1.3 @@ -26,6 +26,7 @@
     1.4  open Sledgehammer_Fact
     1.5  open Sledgehammer_Provers
     1.6  open Sledgehammer_Minimize
     1.7 +open Sledgehammer_Filter_MaSh
     1.8  open Sledgehammer_Run
     1.9  
    1.10  val runN = "run"
    1.11 @@ -35,6 +36,14 @@
    1.12  val running_proversN = "running_provers"
    1.13  val kill_proversN = "kill_provers"
    1.14  val refresh_tptpN = "refresh_tptp"
    1.15 +val mash_resetN = "mash_reset"
    1.16 +val mash_learnN = "mash_learn"
    1.17 +
    1.18 +(* experimental *)
    1.19 +val mash_RESET_N = "mash_RESET"
    1.20 +val mash_ADD_N = "mash_ADD"
    1.21 +val mash_DEL_N = "mash_DEL"
    1.22 +val mash_SUGGEST_N = "mash_SUGGEST"
    1.23  
    1.24  val auto = Unsynchronized.ref false
    1.25  
    1.26 @@ -374,6 +383,18 @@
    1.27        kill_provers ()
    1.28      else if subcommand = refresh_tptpN then
    1.29        refresh_systems_on_tptp ()
    1.30 +    else if subcommand = mash_resetN then
    1.31 +      mash_reset ()
    1.32 +    else if subcommand = mash_learnN then
    1.33 +      () (* TODO: implement *)
    1.34 +    else if subcommand = mash_RESET_N then
    1.35 +      () (* TODO: implement *)
    1.36 +    else if subcommand = mash_ADD_N then
    1.37 +      () (* TODO: implement *)
    1.38 +    else if subcommand = mash_DEL_N then
    1.39 +      () (* TODO: implement *)
    1.40 +    else if subcommand = mash_SUGGEST_N then
    1.41 +      () (* TODO: implement *)
    1.42      else
    1.43        error ("Unknown subcommand: " ^ quote subcommand ^ ".")
    1.44    end