[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