author | wenzelm |
Mon, 24 Oct 2022 20:37:32 +0200 | |
changeset 76371 | 1ac2416e8432 |
parent 76370 | 9bd948666e8a |
child 76372 | 53b5b8883ff7 |
--- 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