* Pure: syntax 'CONST name' produces a fully internalized constant;
authorwenzelm
Wed May 17 22:36:08 2006 +0200 (2006-05-17)
changeset 19682c8c301eb965a
parent 19681 871167b2c70e
child 19683 3620e494cef2
* Pure: syntax 'CONST name' produces a fully internalized constant;
tuned;
NEWS
     1.1 --- a/NEWS	Wed May 17 22:34:52 2006 +0200
     1.2 +++ b/NEWS	Wed May 17 22:36:08 2006 +0200
     1.3 @@ -148,6 +148,16 @@
     1.4  explicit (is "_ ==> ?foo") in the rare cases where this still happens
     1.5  to occur.
     1.6  
     1.7 +* Pure: syntax "CONST name" produces a fully internalized constant
     1.8 +according to the current context.  This is particularly useful for
     1.9 +syntax translations that should refer to internal constant
    1.10 +representations independently of name spaces.
    1.11 +
    1.12 +* Isar/locales: 'const_syntax' provides a robust interface to the
    1.13 +'syntax' primitive that also works in a locale context.  Type
    1.14 +declaration and internal syntactic representation of given constants
    1.15 +retrieved from the context.
    1.16 +
    1.17  * Isar/locales: new derived specification elements 'axiomatization',
    1.18  'definition', 'abbreviation', which support type-inference, admit
    1.19  object-level specifications (equality, equivalence).  See also the
    1.20 @@ -178,10 +188,10 @@
    1.21  'abbreviation' may be used as a type-safe replacement for 'syntax' +
    1.22  'translations' in common applications.
    1.23  
    1.24 -* Isar/locales: 'const_syntax' provides a robust interface to the
    1.25 -'syntax' primitive that also works in a locale context.  Type
    1.26 -declaration and internal syntactic representation of given constants
    1.27 -retrieved from the context.
    1.28 +Concrete syntax is attached to specified constants in internal form,
    1.29 +independently of name spaces.  The parse tree representation is
    1.30 +slightly different -- use 'const_syntax' instead of raw 'syntax', and
    1.31 +'translations' with explicit "CONST" markup to accommodate this.
    1.32  
    1.33  * Provers/induct: improved internal context management to support
    1.34  local fixes and defines on-the-fly.  Thus explicit meta-level