[isabelle-dev] Line breaks in pretty-printed output

Tobias Nipkow nipkow at in.tum.de
Sat Jan 9 15:14:34 CET 2016


One page in Concrete Semantics contains the following output that is a 
pretty-printed HOL formula:

step S27
  (x ::= Plus (V x) (N 1) {{<x := 0>}};;
   x ::= Plus (V x) (N 2) {Q}) =
...

With db9996a84166 it prints like this:

step S27 (x ::= Plus (V x) (N 1) {{<x := 0>}};;
           x ::= Plus (V x) (N 2) {Q}) =
...

While I welcome this change(!), it seems to go against formatting in, for 
example, the Isabelle sources. Not an important point, just curious.

Tobias

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5132 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160109/9973fb52/attachment.p7s>


More information about the isabelle-dev mailing list