# HG changeset patch
# User wenzelm
# Date 1192443031 -7200
# Node ID 7f2e1a8e181b5f87f4ff58a01aeda79767c585a5
# Parent  2ef38332cc7e9fafc5dcbd70ed4858383ee75490
more on authentic syntax;

diff -r 2ef38332cc7e -r 7f2e1a8e181b NEWS
--- a/NEWS	Mon Oct 15 11:59:19 2007 +0200
+++ b/NEWS	Mon Oct 15 12:10:31 2007 +0200
@@ -53,6 +53,15 @@
 type-checking. INCOMPATIBILITY: additional type-constraints (explicit
 'fixes' etc.) are required in rare situations.
 
+* Syntax: constants introduced by new-style packages ('definition',
+'abbreviation' etc.) are passed through the syntax module in
+``authentic mode''. This means that associated mixfix annotations
+really stick to such constants, independently of potential name space
+ambiguities introduced later on. INCOMPATIBILITY: constants in parse
+trees are represented slightly differently, may need to adapt syntax
+translations accordingly. Use CONST marker in 'translations' and
+@{const_syntax} antiquotation in 'parse_translation' etc.
+
 * Legacy goal package: reduced interface to the bare minimum required
 to keep existing proof scripts running.  Most other user-level
 functions are now part of the OldGoals structure, which is *not* open