# HG changeset patch
# User wenzelm
# Date 1147808003 -7200
# Node ID 8885951e9c2df70ff2375452919916da53ac9cc7
# Parent  e1dc01a48a523994539ca03ee927f610449dd2fc
* Isar/locale: 'const_syntax';

diff -r e1dc01a48a52 -r 8885951e9c2d NEWS
--- a/NEWS	Tue May 16 21:33:21 2006 +0200
+++ b/NEWS	Tue May 16 21:33:23 2006 +0200
@@ -148,21 +148,19 @@
 explicit (is "_ ==> ?foo") in the rare cases where this still happens
 to occur.
 
-* Isar/locales: new derived specification elements 'definition',
-'abbreviation', 'axiomatization', which support type-inference, admit
+* Isar/locales: new derived specification elements 'axiomatization',
+'definition', 'abbreviation', which support type-inference, admit
 object-level specifications (equality, equivalence).  See also the
 isar-ref manual.  Examples:
 
+  axiomatization
+    eq  (infix "===" 50)
+    where eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y"
+
   definition
     "f x y = x + y + 1"
     "g x = f x x"
 
-  thm f_def g_def
-
-  axiomatization
-    eq  (infix "===" 50)
-    where eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y"
-
   abbreviation
     neq  (infix "=!=" 50)
     "x =!= y == ~ (x === y)"
@@ -180,6 +178,11 @@
 'abbreviation' may be used as a type-safe replacement for 'syntax' +
 'translations' in common applications.
 
+* Isar/locales: 'const_syntax' provides a robust interface to the
+'syntax' primitive that also works in a locale context.  Type
+declaration and internal syntactic representation of given constants
+retrieved from the context.
+
 * 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