NEWS
changeset 55143 04448228381d
parent 55139 4d899933a51a
child 55152 a56099a6447a
     1.1 --- a/NEWS	Sat Jan 25 21:52:04 2014 +0100
     1.2 +++ b/NEWS	Sat Jan 25 22:06:07 2014 +0100
     1.3 @@ -40,6 +40,10 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Attributes "where" and "of" allow an optional context of local
     1.8 +variables ('for' declaration): these variables become schematic in the
     1.9 +instantiated theorem.
    1.10 +
    1.11  * More thorough check of proof context for goal statements and
    1.12  attributed fact expressions (concerning background theory, declared
    1.13  hyps).  Potential INCOMPATIBILITY, tools need to observe standard
    1.14 @@ -269,6 +273,13 @@
    1.15  
    1.16  *** ML ***
    1.17  
    1.18 +* Proper context discipline for read_instantiate and instantiate_tac:
    1.19 +variables that are meant to become schematic need to be given as
    1.20 +fixed, and are generalized by the explicit context of local variables.
    1.21 +This corresponds to Isar attributes "where" and "of" with 'for'
    1.22 +declaration.  INCOMPATIBILITY, also due to potential change of indices
    1.23 +of schematic variables.
    1.24 +
    1.25  * Toplevel function "use" refers to raw ML bootstrap environment,
    1.26  without Isar context nor antiquotations.  Potential INCOMPATIBILITY.
    1.27  Note that 'ML_file' is the canonical command to load ML files into the