src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 36170 0cdb76723c88
parent 36169 27b1cc58715e
child 36183 f723348b2231
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Apr 16 14:48:34 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Apr 16 15:49:13 2010 +0200
     1.3 @@ -10,13 +10,14 @@
     1.4    val serial_commas : string -> string list -> string list
     1.5    val replace_all : string -> string -> string -> string
     1.6    val remove_all : string -> string -> string
     1.7 +  val timestamp : unit -> string
     1.8    val parse_bool_option : bool -> string -> string -> bool option
     1.9    val parse_time_option : string -> string -> Time.time option
    1.10    val hashw : word * word -> word
    1.11    val hashw_char : Char.char * word -> word
    1.12    val hashw_string : string * word -> word
    1.13  end;
    1.14 -
    1.15 + 
    1.16  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    1.17  struct
    1.18  
    1.19 @@ -40,6 +41,8 @@
    1.20  
    1.21  fun remove_all bef = replace_all bef ""
    1.22  
    1.23 +val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
    1.24 +
    1.25  fun parse_bool_option option name s =
    1.26    (case s of
    1.27       "smart" => if option then NONE else raise Option