1.1 --- a/NEWS	Thu Feb 16 18:26:04 2006 +0100
     1.2 +++ b/NEWS	Thu Feb 16 18:39:48 2006 +0100
     1.3 @@ -115,6 +115,34 @@
     1.4  * Isar: 'obtain' takes an optional case name for the local context
     1.5  introduction rule (default "that").
     1.6  
     1.7 +* Isar/locales: new derived specification elements 'definition',
     1.8 +'abbreviation', 'axiomatization', which support type-inference, admit
     1.9 +object-level specifications (equality, equivalence), and may used
    1.10 +within an optional locale context.  For example:
    1.11 +
    1.12 +  definition
    1.13 +    "f x y = x + y + 1"
    1.14 +    "g x = f x x"
    1.15 +
    1.16 +  thm f_def g_def
    1.17 +
    1.18 +  axiomatization
    1.19 +    eq  (infix "===" 50)
    1.20 +    where eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y"
    1.21 +
    1.22 +  abbreviation (output)
    1.23 +    neq  (infix "=!=" 50)
    1.24 +    "(x =!= y) <-> ~ (x === y)"
    1.25 +
    1.26 +Within a locale context, constants being introduced depend on certain
    1.27 +fixed parameters, and the constant name is qualified by the locale
    1.28 +base name.  An internal abbreviation takes care for convenient input
    1.29 +and output, making the parameters implicit and using the original
    1.30 +short name.  Presently, abbreviations are only available "in" a target
    1.31 +locale, but not inherited by general import expressions.
    1.32 +
    1.33 +See the isar-ref manual for further details.
    1.34 +
    1.35  * Provers/induct: improved internal context management to support
    1.36  local fixes and defines on-the-fly.  Thus explicit meta-level
    1.37  connectives !! and ==> are rarely required anymore in inductive goals
    1.38 @@ -363,8 +391,8 @@
    1.39  * Pure/General/rat.ML implements rational numbers.
    1.40  
    1.41  * Pure/General/table.ML: the join operations now works via exceptions
    1.42 -DUP/SAME instead of type option.  This is both simpler and admits
    1.43 -slightly more efficient complex applications.
    1.44 +DUP/SAME instead of type option.  This is simpler in simple cases, and
    1.45 +admits slightly more efficient complex applications.
    1.46  
    1.47  * Pure: datatype Context.generic joins theory/Proof.context and
    1.48  provides some facilities for code that works in either kind of