# HG changeset patch
# User nipkow
# Date 1515596275 -3600
# Node ID bbed46f40cf56354cea7882af005a37993b4eed5
# Parent  eab6ce8368fa1bc53f25526c474a7638b8a3a332
tuned

diff -r eab6ce8368fa -r bbed46f40cf5 NEWS
--- a/NEWS	Wed Jan 10 15:25:09 2018 +0100
+++ b/NEWS	Wed Jan 10 15:57:55 2018 +0100
@@ -10,7 +10,9 @@
 *** General ***
 
 * The "op <infix-op>" syntax for infix opertors has been replaced by
-"(<infix-op>)". INCOMPATIBILITY.
+"(<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