* Pure: syntax constant for foo (binder) is called foo_binder;
authorwenzelm
Sun Nov 26 18:07:36 2006 +0100 (2006-11-26)
changeset 2153745b3a85ee548
parent 21536 f119c730f509
child 21538 678299eac351
* Pure: syntax constant for foo (binder) is called foo_binder;
NEWS
     1.1 --- a/NEWS	Sun Nov 26 18:07:35 2006 +0100
     1.2 +++ b/NEWS	Sun Nov 26 18:07:36 2006 +0100
     1.3 @@ -239,6 +239,10 @@
     1.4  syntax translations that should refer to internal constant
     1.5  representations independently of name spaces.
     1.6  
     1.7 +* Pure: syntax constant for foo (binder "FOO ") is called "foo_binder"
     1.8 +instead of "FOO ". This allows multiple binder declarations to coexist
     1.9 +in the same context.  INCOMPATIBILITY.
    1.10 +
    1.11  * Isar/locales: 'notation' provides a robust interface to the 'syntax'
    1.12  primitive that also works in a locale context (both for constants and
    1.13  fixed variables).  Type declaration and internal syntactic