| changeset 76371 | 1ac2416e8432 |
| parent 74884 | 229d7ea628c2 |
| child 76955 | 3f25c28c4257 |
--- a/src/Pure/Thy/latex.ML Mon Oct 24 20:24:34 2022 +0200 +++ b/src/Pure/Thy/latex.ML Mon Oct 24 20:37:32 2022 +0200 @@ -14,6 +14,7 @@ val macro0: string -> text val macro: string -> text -> text val environment: string -> text -> text + val output_name: string -> string val output_ascii: string -> string val output_ascii_breakable: string -> string -> string val output_symbols: Symbol.symbol list -> string