output \isachar;
authorwenzelm
Sat Aug 19 12:49:19 2000 +0200 (2000-08-19)
changeset 9663e4d58f1be05b
parent 9662 896f5c5cfc56
child 9664 4cae97480a6d
output \isachar;
src/Pure/Thy/latex.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Sat Aug 19 12:48:26 2000 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Sat Aug 19 12:49:19 2000 +0200
     1.3 @@ -28,17 +28,27 @@
     1.4  val output_chr = fn
     1.5    " " => "\\ " |
     1.6    "\n" => "\\isanewline\n" |
     1.7 -  "$" => "\\$" |
     1.8 -  "&" => "\\&" |
     1.9 -  "%" => "\\%" |
    1.10 -  "#" => "\\#" |
    1.11 -  "_" => "\\_" |
    1.12 -  "{" => "{\\isabraceleft}" |
    1.13 -  "}" => "{\\isabraceright}" |
    1.14 -  "~" => "{\\isatilde}" |
    1.15 -  "^" => "{\\isacircum}" |
    1.16 -  "\"" => "{\"}" |
    1.17 -  "\\" => "{\\isabackslash}" |
    1.18 +  "#" => "{\\isacharhash}" |
    1.19 +  "$" => "{\\isachardollar}" |
    1.20 +  "%" => "{\\isacharpercent}" |
    1.21 +  "&" => "{\\isacharampersand}" |
    1.22 +  "'" => "{\\isacharprime}" |
    1.23 +  "(" => "{\\isacharparenleft}" |
    1.24 +  ")" => "{\\isacharparenright}" |
    1.25 +  "*" => "{\\isacharasterisk}" |
    1.26 +  "-" => "{\\isacharminus}" |
    1.27 +  "<" => "{\\isacharless}" |
    1.28 +  ">" => "{\\isachargreater}" |
    1.29 +  "[" => "{\\isacharbrackleft}" |
    1.30 +  "\"" => "{\\isachardoublequote}" |
    1.31 +  "\\" => "{\\isacharbackslash}" |
    1.32 +  "]" => "{\\isacharbrackright}" |
    1.33 +  "^" => "{\\isacharcircum}" |
    1.34 +  "_" => "{\\isacharunderscore}" |
    1.35 +  "{" => "{\\isacharbraceleft}" |
    1.36 +  "|" => "{\\isacharbar}" |
    1.37 +  "}" => "{\\isacharbraceright}" |
    1.38 +  "~" => "{\\isachartilde}" |
    1.39    c => c;
    1.40  
    1.41  fun output_sym s =