NEWS
changeset 15727 b43d82139a6c
parent 15724 1b89c781a7ec
child 15744 daa84ebbdf94
     1.1 --- a/NEWS	Wed Apr 13 18:51:39 2005 +0200
     1.2 +++ b/NEWS	Wed Apr 13 20:20:14 2005 +0200
     1.3 @@ -161,6 +161,27 @@
     1.4    in duplicate.
     1.5    Use print_interps to inspect active interpretations of a particular locale.
     1.6  
     1.7 +* Locales: proper static binding of attribute syntax -- i.e. types /
     1.8 +  terms / facts mentioned as arguments are always those of the locale
     1.9 +  definition context, independently of the context of later
    1.10 +  invocations.  Moreover, locale operations (renaming and type / term
    1.11 +  instantiation) are applied to attribute arguments as expected.
    1.12 +
    1.13 +  INCOMPATIBILITY of the ML interface: always pass Attrib.src instead
    1.14 +  of actual attributes; rare situations may require Attrib.attribute
    1.15 +  to embed those attributes into Attrib.src that lack concrete syntax.
    1.16 +
    1.17 +  Attribute implementations need to cooperate properly with the static
    1.18 +  binding mechanism.  Basic parsers Args.XXX_typ/term/prop and
    1.19 +  Attrib.XXX_thm etc. already do the right thing without further
    1.20 +  intervention.  Only unusual applications -- such as "where" or "of"
    1.21 +  (cf. src/Pure/Isar/attrib.ML), which process arguments depending
    1.22 +  both on the context and the facts involved -- may have to assign
    1.23 +  parsed values to argument tokens explicitly.
    1.24 +
    1.25 +* Attributes 'induct' and 'cases': type or set names may now be
    1.26 +  locally fixed variables as well.
    1.27 +
    1.28  * Isar: new syntax 'name(i-j, i-, i, ...)' for referring to specific
    1.29    selections of theorems in named facts via indices.
    1.30  
    1.31 @@ -2985,4 +3006,3 @@
    1.32  
    1.33  
    1.34  $Id$
    1.35 -