[isabelle-dev] proof state layout

Tobias Nipkow nipkow at in.tum.de
Tue Jul 28 07:54:24 CEST 2020


Thanks, back to normal!

Tobias

On 26/07/2020 22:41, Makarius wrote:
> 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
> https://isabelle-dev.sketis.net/rISABELLE9c0b835d4cc2
> 
> 
> 	Makarius
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5579 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20200728/69b97cb4/attachment.bin>


More information about the isabelle-dev mailing list