author | wenzelm |
Mon, 04 Sep 2000 18:38:53 +0200 | |
changeset 9828 | 1d8bc4f1833e |
parent 9827 | ce6e22ff89c3 |
child 9829 | bf49c3796599 |
--- a/src/Pure/Isar/isar_output.ML Mon Sep 04 11:21:24 2000 +0200 +++ b/src/Pure/Isar/isar_output.ML Mon Sep 04 18:38:53 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 "%\n\\begin{isabelle}%\n" "%\n\\end{isabelle}%\n" else Pretty.str_of prt |> enclose "\\isa{" "}";