1.1 --- a/NEWS	Tue May 16 21:33:21 2006 +0200
     1.2 +++ b/NEWS	Tue May 16 21:33:23 2006 +0200
     1.3 @@ -148,21 +148,19 @@
     1.4  explicit (is "_ ==> ?foo") in the rare cases where this still happens
     1.5  to occur.
     1.6  
     1.7 -* Isar/locales: new derived specification elements 'definition',
     1.8 -'abbreviation', 'axiomatization', which support type-inference, admit
     1.9 +* Isar/locales: new derived specification elements 'axiomatization',
    1.10 +'definition', 'abbreviation', which support type-inference, admit
    1.11  object-level specifications (equality, equivalence).  See also the
    1.12  isar-ref manual.  Examples:
    1.13  
    1.14 +  axiomatization
    1.15 +    eq  (infix "===" 50)
    1.16 +    where eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y"
    1.17 +
    1.18    definition
    1.19      "f x y = x + y + 1"
    1.20      "g x = f x x"
    1.21  
    1.22 -  thm f_def g_def
    1.23 -
    1.24 -  axiomatization
    1.25 -    eq  (infix "===" 50)
    1.26 -    where eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y"
    1.27 -
    1.28    abbreviation
    1.29      neq  (infix "=!=" 50)
    1.30      "x =!= y == ~ (x === y)"
    1.31 @@ -180,6 +178,11 @@
    1.32  'abbreviation' may be used as a type-safe replacement for 'syntax' +
    1.33  'translations' in common applications.
    1.34  
    1.35 +* Isar/locales: 'const_syntax' provides a robust interface to the
    1.36 +'syntax' primitive that also works in a locale context.  Type
    1.37 +declaration and internal syntactic representation of given constants
    1.38 +retrieved from the context.
    1.39 +
    1.40  * Provers/induct: improved internal context management to support
    1.41  local fixes and defines on-the-fly.  Thus explicit meta-level
    1.42  connectives !! and ==> are rarely required anymore in inductive goals