# HG changeset patch
# User wenzelm
# Date 966682159 -7200
# Node ID e4d58f1be05b8476b63041e1f7132cb1fa66ea5e
# Parent  896f5c5cfc560ab6373508b165d4f7ff22744dc4
output \isachar;

diff -r 896f5c5cfc56 -r e4d58f1be05b src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sat Aug 19 12:48:26 2000 +0200
+++ b/src/Pure/Thy/latex.ML	Sat Aug 19 12:49:19 2000 +0200
@@ -28,17 +28,27 @@
 val output_chr = fn
   " " => "\\ " |
   "\n" => "\\isanewline\n" |
-  "$" => "\\$" |
-  "&" => "\\&" |
-  "%" => "\\%" |
-  "#" => "\\#" |
-  "_" => "\\_" |
-  "{" => "{\\isabraceleft}" |
-  "}" => "{\\isabraceright}" |
-  "~" => "{\\isatilde}" |
-  "^" => "{\\isacircum}" |
-  "\"" => "{\"}" |
-  "\\" => "{\\isabackslash}" |
+  "#" => "{\\isacharhash}" |
+  "$" => "{\\isachardollar}" |
+  "%" => "{\\isacharpercent}" |
+  "&" => "{\\isacharampersand}" |
+  "'" => "{\\isacharprime}" |
+  "(" => "{\\isacharparenleft}" |
+  ")" => "{\\isacharparenright}" |
+  "*" => "{\\isacharasterisk}" |
+  "-" => "{\\isacharminus}" |
+  "<" => "{\\isacharless}" |
+  ">" => "{\\isachargreater}" |
+  "[" => "{\\isacharbrackleft}" |
+  "\"" => "{\\isachardoublequote}" |
+  "\\" => "{\\isacharbackslash}" |
+  "]" => "{\\isacharbrackright}" |
+  "^" => "{\\isacharcircum}" |
+  "_" => "{\\isacharunderscore}" |
+  "{" => "{\\isacharbraceleft}" |
+  "|" => "{\\isacharbar}" |
+  "}" => "{\\isacharbraceright}" |
+  "~" => "{\\isachartilde}" |
   c => c;
 
 fun output_sym s =