[isabelle-dev] NEWS: op <infix> -> (<infix>)
makarius at sketis.net
Thu Jan 11 14:27:31 CET 2018
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 --
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.
More information about the isabelle-dev