[isabelle-dev] NEWS: op <infix> -> (<infix>)

[Makarius]

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
description:
New infix syntax: 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.


	Makarius