author | wenzelm |
Tue, 05 Sep 2000 18:51:25 +0200 | |
changeset 9863 | 67cdb658e422 |
parent 9862 | 96138f29545e |
child 9864 | b4a170f7d658 |
--- a/src/Pure/Isar/isar_output.ML Tue Sep 05 18:50:52 2000 +0200 +++ b/src/Pure/Isar/isar_output.ML Tue Sep 05 18:51:25 2000 +0200 @@ -271,7 +271,7 @@ fun cond_display prt = if ! display then Pretty.string_of (Pretty.indent (! indent) prt) - |> enclose "%\n\\begin{isabelle}%\n" "%\n\\end{isabelle}%\n" + |> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" else Pretty.str_of prt |> enclose "\\isa{" "}";