On 10/01/2018 21:23, Makarius wrote:
On 10/01/18 20:17, Tobias Nipkow wrote:
Invoking "isabelle
update_op" converts all files in the current directory (recursively).
In case you want to exclude conversion of ML files (because the tool
frequently also converts ML's "op" syntax), use option "-m".

In revision eab6ce8368fa

These are more changes than I expected, but even that is to be expected
with the wealth of material we have accumulated :-)

BTW, in the follow-up change a82df75b7f85 ("tuned notation") the special
breaks introduced by Larry in 1996 got lost:

changeset:   2006:72754e060aa2
user:        paulson
date:        Mon Sep 23 17:47:49 1996 +0200
files:       src/HOL/Ord.thy src/HOL/Set.thy
New infix syntax: breaks line BEFORE operator

I did wonder if it had been done on purpose and toyed with the idea of consulting the history but the "uniformity" drive won. Thanks for keeping me honest. But I do wonder: shouldn't all infix operators be printed in the same manner? Having the operator on the new line in case of a break makes a lot of sense to me because it clearly how this line is connected with the previous one. [I seem to remember Lamport makes a similar point but it is not in his "How to write a proof".]

How about a uniform change to "breaks line BEFORE operator"?


Larry has recently done analogous changes (e.g. bdf25939a550), so it
appears to be still the state-of-the art to have these exceptions in
pretty printing.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

isabelle-dev mailing list

Reply via email to