Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] proof state layout

view this post on Zulip Email Gateway (Jul 24 2020 at 11:34):

From: Tobias Nipkow <>
When I look at how proof states are displayed in the document prog-prove.pdf
dated April 29 it looks like it always did. However, when I produced the same
document today I find that the pretty printer no longer inserts line breaks in
subgoals but displays them as one long line. For example on page 11. What
happened and how can I get the line breaks back?


view this post on Zulip Email Gateway (Jul 26 2020 at 20:42):

From: Makarius <>
OK, this is a consequence of pide_session=true, which is now enabled by default.

I have updated the latex pretty-printing accordingly, so it should work again, see


isabelle-dev mailing list

view this post on Zulip Email Gateway (Jul 28 2020 at 05:54):

From: Tobias Nipkow <>
Thanks, back to normal!


Last updated: Mar 04 2024 at 10:08 UTC