--- a/NEWS Wed Jun 01 10:52:17 2005 +0200
+++ b/NEWS Wed Jun 01 12:30:49 2005 +0200
@@ -141,8 +141,11 @@
- Fixed parameter management in theorem generation for goals with "includes".
INCOMPATIBILITY: rarely, the generated theorem statement is different.
-* Locales: locale expressions permit optional mixfix redeclaration for
- renamed parameters.
+* Locales: new context element "constrains" for adding type constraints
+ to parameters.
+
+* Locales: context expressions permit optional syntax redeclaration when
+ renaming parameters.
* Locales: new commands for the interpretation of locale expressions
in theories (interpretation) and proof contexts (interpret). These take an
@@ -155,6 +158,9 @@
Use print_interps to inspect active interpretations of a particular locale.
For details, see the Isar Reference manual.
+* Locales: INCOMPATIBILITY: experimental command "instantiate" has
+ been withdrawn. Use "interpret" instead.
+
* Locales: proper static binding of attribute syntax -- i.e. types /
terms / facts mentioned as arguments are always those of the locale
definition context, independently of the context of later