--- a/NEWS Sat Jan 25 21:52:04 2014 +0100
+++ b/NEWS Sat Jan 25 22:06:07 2014 +0100
@@ -40,6 +40,10 @@
*** Pure ***
+* Attributes "where" and "of" allow an optional context of local
+variables ('for' declaration): these variables become schematic in the
+instantiated theorem.
+
* More thorough check of proof context for goal statements and
attributed fact expressions (concerning background theory, declared
hyps). Potential INCOMPATIBILITY, tools need to observe standard
@@ -269,6 +273,13 @@
*** ML ***
+* Proper context discipline for read_instantiate and instantiate_tac:
+variables that are meant to become schematic need to be given as
+fixed, and are generalized by the explicit context of local variables.
+This corresponds to Isar attributes "where" and "of" with 'for'
+declaration. INCOMPATIBILITY, also due to potential change of indices
+of schematic variables.
+
* Toplevel function "use" refers to raw ML bootstrap environment,
without Isar context nor antiquotations. Potential INCOMPATIBILITY.
Note that 'ML_file' is the canonical command to load ML files into the