author | wenzelm |
Tue, 16 Jan 2001 21:53:57 +0100 | |
changeset 10923 | e34948f18541 |
parent 10922 | f1209aff9517 |
child 10924 | 92305ae9f460 |
--- a/src/Pure/General/symbol.ML Tue Jan 16 19:22:13 2001 +0100 +++ b/src/Pure/General/symbol.ML Tue Jan 16 21:53:57 2001 +0100 @@ -38,6 +38,7 @@ val isabelle_fontN: string val symbolsN: string val xsymbolsN: string + val plain_output: string -> string val output: string -> string val output_width: string -> string * real end; @@ -353,6 +354,7 @@ | Some f => f s); val output = #1 o output_width; +val plain_output = #1 o default_output; (*final declarations of this structure!*)