[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".

I've made some minor amendments here (which was simple thanks to Poly/ML
warnings): e9ab4ad7bd15 "uniform use of Standard ML op-infix --
eliminated warnings;"

Theoretically, one could force our version of "Standard ML embraced and
extended" to accept (infix-op) notation without warning, but I don't
feel like burning all bridges towards regular SML: the Prover IDE
actually supports that language, too, even though hardly anybody uses it.


	Makarius