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

[Tobias Nipkow]

* The "op <infix-op>" syntax for infix operators has been replaced by
"(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to
be a space between the "*" and the corresponding parenthesis.
INCOMPATIBILITY.
There is an Isabelle tool "update_op" that converts theory and ML files
to the new syntax. Because it is based on regular expression matching,
the result may need a bit of manual postprocessing. 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180110/cea94c32/attachment.p7s>