NEWS
changeset 67398 5eb932e604a2
parent 67395 b39d596b77ce
child 67400 bbed46f40cf5
     1.1 --- a/NEWS	Wed Jan 10 13:35:56 2018 +0100
     1.2 +++ b/NEWS	Wed Jan 10 15:21:49 2018 +0100
     1.3 @@ -9,6 +9,15 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* The "op <infix-op>" syntax for infix opertors has been replaced by
     1.8 +"(<infix-op>)". INCOMPATIBILITY.
     1.9 +There is an Isabelle tool "update_op" that converts theory and ML files
    1.10 +to the new syntax. Because it is based on regular expression matching,
    1.11 +the result may need a bit of manual postprocessing. Invoking "isabelle
    1.12 +update_op" converts all files in the current directory (recursively).
    1.13 +In case you want to exclude conversion of ML files (because the tool
    1.14 +frequently also converts ML's "op" syntax), use option "-m".
    1.15 +
    1.16  * The old 'def' command has been discontinued (legacy since
    1.17  Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
    1.18  object-logic equality or equivalence.