src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 36486 c2d7e2dff59e
parent 36478 1aba777a367f
child 36491 6769f8eacaac
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Apr 27 18:58:05 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 28 12:46:50 2010 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4    val timestamp : unit -> string
     1.5    val parse_bool_option : bool -> string -> string -> bool option
     1.6    val parse_time_option : string -> string -> Time.time option
     1.7 +  val nat_subscript : int -> string
     1.8    val unyxml : string -> string
     1.9    val maybe_quote : string -> string
    1.10  end;
    1.11 @@ -74,6 +75,9 @@
    1.12          SOME (Time.fromMilliseconds msecs)
    1.13      end
    1.14  
    1.15 +val subscript = implode o map (prefix "\<^isub>") o explode
    1.16 +val nat_subscript = subscript o string_of_int
    1.17 +
    1.18  fun plain_string_from_xml_tree t =
    1.19    Buffer.empty |> XML.add_content t |> Buffer.content
    1.20  val unyxml = plain_string_from_xml_tree o YXML.parse