equal
deleted
inserted
replaced
6 LaTeX presentation primitives (based on outer lexical syntax). |
6 LaTeX presentation primitives (based on outer lexical syntax). |
7 *) |
7 *) |
8 |
8 |
9 signature LATEX = |
9 signature LATEX = |
10 sig |
10 sig |
|
11 val output_symbols: Symbol.symbol list -> string |
11 datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim |
12 datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim |
12 val output_tokens: (token * string) list -> string |
13 val output_tokens: (token * string) list -> string |
13 val tex_trailer: string |
14 val tex_trailer: string |
14 val isabelle_file: string -> string -> string |
15 val isabelle_file: string -> string -> string |
15 val old_symbol_source: string -> Symbol.symbol list -> string |
16 val old_symbol_source: string -> Symbol.symbol list -> string |