--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Apr 27 18:58:05 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Apr 28 12:46:50 2010 +0200
@@ -14,6 +14,7 @@
val timestamp : unit -> string
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
+ val nat_subscript : int -> string
val unyxml : string -> string
val maybe_quote : string -> string
end;
@@ -74,6 +75,9 @@
SOME (Time.fromMilliseconds msecs)
end
+val subscript = implode o map (prefix "\<^isub>") o explode
+val nat_subscript = subscript o string_of_int
+
fun plain_string_from_xml_tree t =
Buffer.empty |> XML.add_content t |> Buffer.content
val unyxml = plain_string_from_xml_tree o YXML.parse