[isabelle-dev] proof state layout

Makarius makarius at sketis.net
Sun Jul 26 22:41:58 CEST 2020

On 24/07/2020 13:34, Tobias Nipkow wrote:
> 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?

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


More information about the isabelle-dev mailing list