src/HOL/Tools/Sledgehammer/sledgehammer_util.ML

   val replace_all : string -> string -> string -> string
   val remove_all : string -> string -> string
   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;
  
 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =

                \value (e.g., \"60 s\", \"200 ms\") or \"none\".")
       else
         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
 
 val is_long_identifier = forall Syntax.is_identifier o space_explode "."