NEWS
changeset 23920 4288dc7dc248
parent 23889 1794f405eacc
child 23971 e6d505d5b03d
     1.1 --- a/NEWS	Mon Jul 23 13:48:30 2007 +0200
     1.2 +++ b/NEWS	Mon Jul 23 13:50:31 2007 +0200
     1.3 @@ -364,6 +364,18 @@
     1.4  has changed.  This enables to override declarations from fragments due
     1.5  to interpretations -- for example, unwanted simp rules.
     1.6  
     1.7 +* Isar/locales: interpretation in theories and proof contexts has been
     1.8 +extended.  One may now specify (and prove) equations, which are
     1.9 +unfolded in interpreted theorems.  This is useful for replacing
    1.10 +defined concepts (constants depending on locale parameters) by
    1.11 +concepts already existing in the target context.  Example:
    1.12 +
    1.13 +  interpretation partial_order ["op <= :: [int, int] => bool"]
    1.14 +    where "partial_order.less (op <=) (x::int) y = (x < y)"
    1.15 +
    1.16 +Typically, the constant `partial_order.less' is created by the
    1.17 +specification element definition in the context of locale partial_order.
    1.18 +
    1.19  * Provers/induct: improved internal context management to support
    1.20  local fixes and defines on-the-fly.  Thus explicit meta-level
    1.21  connectives !! and ==> are rarely required anymore in inductive goals