changeset 43709 | 717e96cf9527 |
parent 43485 | 33a24212a72d |
child 45666 | d83797ef0d2d |
--- a/src/Pure/Thy/latex.ML Fri Jul 08 16:01:14 2011 +0200 +++ b/src/Pure/Thy/latex.ML Fri Jul 08 16:13:34 2011 +0200 @@ -83,6 +83,7 @@ ("~", "{\\isachartilde}")]; fun output_chr " " = "\\ " + | output_chr "\t" = "\\ " | output_chr "\n" = "\\isanewline\n" | output_chr c = (case Symtab.lookup char_table c of