export attribute;
authorwenzelm
Sat Jul 07 12:16:20 2007 +0200 (2007-07-07)
changeset 23632a7df2990f127
parent 23631 2a9e918653cc
child 23633 f25b1566f7b5
export attribute;
src/Pure/Tools/xml.ML
     1.1 --- a/src/Pure/Tools/xml.ML	Sat Jul 07 12:16:19 2007 +0200
     1.2 +++ b/src/Pure/Tools/xml.ML	Sat Jul 07 12:16:20 2007 +0200
     1.3 @@ -13,6 +13,7 @@
     1.4    val text_charref: string -> string
     1.5    val cdata: string -> string
     1.6    type attributes = (string * string) list
     1.7 +  val attribute: string * string -> string
     1.8    val element: string -> attributes -> string list -> string
     1.9    (* tree functions *)
    1.10    datatype tree =