author | berghofe |
Wed, 10 Oct 2001 18:41:13 +0200 | |
changeset 11719 | 49c14348a42b |
parent 11718 | 92706a69dacc |
child 11720 | 5341e38309e8 |
--- 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