NEWS
changeset 19083 6618203f8032
parent 19081 085b5badb8de
child 19084 19620462f4a6
     1.1 --- a/NEWS	Thu Feb 16 18:59:39 2006 +0100
     1.2 +++ b/NEWS	Thu Feb 16 19:10:47 2006 +0100
     1.3 @@ -117,8 +117,8 @@
     1.4  
     1.5  * Isar/locales: new derived specification elements 'definition',
     1.6  'abbreviation', 'axiomatization', which support type-inference, admit
     1.7 -object-level specifications (equality, equivalence), and may used
     1.8 -within an optional locale context.  For example:
     1.9 +object-level specifications (equality, equivalence).  See also the
    1.10 +isar-ref manual.  Examples:
    1.11  
    1.12    definition
    1.13      "f x y = x + y + 1"
    1.14 @@ -134,14 +134,16 @@
    1.15      neq  (infix "=!=" 50)
    1.16      "(x =!= y) <-> ~ (x === y)"
    1.17  
    1.18 -Within a locale context, constants being introduced depend on certain
    1.19 -fixed parameters, and the constant name is qualified by the locale
    1.20 -base name.  An internal abbreviation takes care for convenient input
    1.21 -and output, making the parameters implicit and using the original
    1.22 -short name.  Presently, abbreviations are only available "in" a target
    1.23 -locale, but not inherited by general import expressions.
    1.24 -
    1.25 -See the isar-ref manual for further details.
    1.26 +These specifications may be also used in a locale context.  Then the
    1.27 +constants being introduced depend on certain fixed parameters, and the
    1.28 +constant name is qualified by the locale base name.  An internal
    1.29 +abbreviation takes care for convenient input and output, making the
    1.30 +parameters implicit and using the original short name.  See
    1.31 +HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic
    1.32 +entities from a monomorphic theory.
    1.33 +
    1.34 +Presently, abbreviations are only available 'in' a target locale, but
    1.35 +not inherited by general import expressions.
    1.36  
    1.37  * Provers/induct: improved internal context management to support
    1.38  local fixes and defines on-the-fly.  Thus explicit meta-level