improved output of space symbol;
authorwenzelm
Thu Aug 03 00:44:08 2000 +0200 (2000-08-03)
changeset 950509c75c801dde
parent 9504 8168600e88a5
child 9506 e5857656b8f0
improved output of space symbol;
src/Pure/Thy/latex.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Thu Aug 03 00:41:07 2000 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Thu Aug 03 00:44:08 2000 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  local
     1.5  
     1.6  val output_chr = fn
     1.7 -  " " => "~" |
     1.8 +  " " => "\\ " |
     1.9    "\n" => "\\isanewline\n" |
    1.10    "$" => "\\$" |
    1.11    "&" => "\\&" |