src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 59431 db440f97cf1a
parent 59058 a78612c67ec0
child 59433 9da5b2c61049
equal deleted inserted replaced
59430:b65809f05dc9 59431:db440f97cf1a
    68   exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *)
    68   exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *)
    69 
    69 
    70 fun parse_time name s =
    70 fun parse_time name s =
    71   let val secs = if has_junk s then NONE else Real.fromString s in
    71   let val secs = if has_junk s then NONE else Real.fromString s in
    72     if is_none secs orelse Real.< (the secs, 0.0) then
    72     if is_none secs orelse Real.< (the secs, 0.0) then
    73       error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \number of seconds \
    73       error ("Parameter " ^ quote name ^ " must be assigned a nonnegative number of seconds \
    74         \(e.g., \"60\", \"0.5\") or \"none\".")
    74         \(e.g., \"60\", \"0.5\") or \"none\".")
    75     else
    75     else
    76       seconds (the secs)
    76       seconds (the secs)
    77   end
    77   end
    78 
    78