Exported output_symbols.
authorberghofe
Wed Oct 10 18:41:13 2001 +0200 (2001-10-10)
changeset 1171949c14348a42b
parent 11718 92706a69dacc
child 11720 5341e38309e8
Exported output_symbols.
src/Pure/Thy/latex.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Wed Oct 10 18:40:46 2001 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Wed Oct 10 18:41:13 2001 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  
     1.5  signature LATEX =
     1.6  sig
     1.7 +  val output_symbols: Symbol.symbol list -> string
     1.8    datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim
     1.9    val output_tokens: (token * string) list -> string
    1.10    val tex_trailer: string