changeset 8117 | 0a6173c9b2d0 |
parent 7973 | 0d801c6e4dc0 |
child 8192 | 45a7027136e3 |
--- a/src/Pure/Thy/latex.ML Mon Jan 10 16:07:29 2000 +0100 +++ b/src/Pure/Thy/latex.ML Mon Jan 10 17:08:41 2000 +0100 @@ -87,7 +87,7 @@ (* theory presentation *) fun token_source toks = - "\\begin{isabellesimple}\n" ^ output_tokens toks ^ "\\end{isabellesimple}\n"; + "\\begin{isabellesimple}%\n" ^ output_tokens toks ^ "\\end{isabellesimple}\n"; fun theory_entry name = "\\input{" ^ name ^ ".tex}\n";