src/Pure/Thy/latex.ML
changeset 9144 20a70ef9c320
parent 9135 3aa95ab3f02d
child 9505 09c75c801dde
     1.1 --- a/src/Pure/Thy/latex.ML	Mon Jun 26 00:00:40 2000 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Mon Jun 26 00:23:17 2000 +0200
     1.3 @@ -104,7 +104,7 @@
     1.4    \%%% Local Variables:\n\
     1.5    \%%% mode: latex\n\
     1.6    \%%% TeX-master: \"root\"\n\
     1.7 -  \%%% End:\n%";
     1.8 +  \%%% End:\n";
     1.9  
    1.10  fun old_symbol_source name syms =
    1.11    isabelle_file ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms);