--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jul 20 22:19:46 2012 +0200
@@ -6,6 +6,7 @@
signature SLEDGEHAMMER_UTIL =
sig
+ val sledgehammerN : string
val plural_s : int -> string
val serial_commas : string -> string list -> string list
val simplify_spaces : string -> string
@@ -23,6 +24,8 @@
open ATP_Util
+val sledgehammerN = "sledgehammer"
+
fun plural_s n = if n = 1 then "" else "s"
val serial_commas = Try.serial_commas