tuned;
authorwenzelm
Mon Jun 26 00:23:17 2000 +0200 (2000-06-26)
changeset 914420a70ef9c320
parent 9143 6180c29d2db6
child 9145 9f7b8de5bfaf
tuned;
src/Pure/Thy/latex.ML
     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);