| changeset 11719 | 49c14348a42b |
| parent 11012 | 8eb472444705 |
| child 11860 | 36ba0d4a836c |
--- a/src/Pure/Thy/latex.ML Wed Oct 10 18:40:46 2001 +0200 +++ b/src/Pure/Thy/latex.ML Wed Oct 10 18:41:13 2001 +0200 @@ -8,6 +8,7 @@ signature LATEX = sig + val output_symbols: Symbol.symbol list -> string datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim val output_tokens: (token * string) list -> string val tex_trailer: string