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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
