src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

   type reconstructor = ATP_Reconstruct.reconstructor
   type play = ATP_Reconstruct.play
   type minimize_command = ATP_Reconstruct.minimize_command
   type relevance_fudge = Sledgehammer_Filter.relevance_fudge
 
-  datatype mode = Auto_Try | Try | Normal | Minimize
+  datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
 
   type params =
     {debug: bool,
      verbose: bool,
      overlord: bool,

 open Sledgehammer_Util
 open Sledgehammer_Filter
 
 (** The Sledgehammer **)
 
-datatype mode = Auto_Try | Try | Normal | Minimize
+datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
 
 (* Identifier that distinguishes Sledgehammer from other tools that could use
    "Async_Manager". *)
 val das_tool = "Sledgehammer"
 

   #> Config.put Monomorph.keep_partial_instances false
 
 fun suffix_for_mode Auto_Try = "_auto_try"
   | suffix_for_mode Try = "_try"
   | suffix_for_mode Normal = ""
+  | suffix_for_mode Auto_Minimize = "_auto_min"
   | suffix_for_mode Minimize = "_min"
 
 (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on
    Linux appears to be the only ATP that does not honor its time limit. *)
 val atp_timeout_slack = seconds 1.0