tuned
authornipkow
Wed Jan 10 15:57:55 2018 +0100 (17 months ago)
changeset 67400bbed46f40cf5
parent 67399 eab6ce8368fa
child 67401 a82df75b7f85
tuned
NEWS
     1.1 --- a/NEWS	Wed Jan 10 15:25:09 2018 +0100
     1.2 +++ b/NEWS	Wed Jan 10 15:57:55 2018 +0100
     1.3 @@ -10,7 +10,9 @@
     1.4  *** General ***
     1.5  
     1.6  * The "op <infix-op>" syntax for infix opertors has been replaced by
     1.7 -"(<infix-op>)". INCOMPATIBILITY.
     1.8 +"(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to
     1.9 +be a space between the "*" and the corresponding parenthesis.
    1.10 +INCOMPATIBILITY.
    1.11  There is an Isabelle tool "update_op" that converts theory and ML files
    1.12  to the new syntax. Because it is based on regular expression matching,
    1.13  the result may need a bit of manual postprocessing. Invoking "isabelle