--- a/NEWS Tue Jun 06 09:28:24 2006 +0200
+++ b/NEWS Tue Jun 06 10:05:57 2006 +0200
@@ -196,6 +196,12 @@
slightly different -- use 'const_syntax' instead of raw 'syntax', and
'translations' with explicit "CONST" markup to accommodate this.
+* Isar/locales: improved parameter handling:
+- use of locales "var" and "struct" no longer necessary;
+- parameter renamings are no longer required to be injective.
+ This enables, for example, to define a locale for endomorphisms thus:
+ locale endom = homom mult mult h.
+
* Provers/induct: improved internal context management to support
local fixes and defines on-the-fly. Thus explicit meta-level
connectives !! and ==> are rarely required anymore in inductive goals