diff -r cefceb54c656 -r c7faa011bfa7 NEWS
--- a/NEWS	Thu Feb 16 17:09:15 2012 +0100
+++ b/NEWS	Thu Feb 16 22:18:28 2012 +0100
@@ -36,6 +36,10 @@
 "num_position" etc. are mainly used instead (which also include
 position information via constraints).
 
+* Simplified configuration options for syntax ambiguity: see
+"syntax_ambiguity" and "syntax_ambiguity_limit" in isar-ref manual.
+Minor INCOMPATIBILITY.
+
 
 *** Pure ***