NEWS
changeset 28710 e2064974c114
parent 28700 fb92b1d1b285
child 28741 1b257449f804
     1.1 --- a/NEWS	Wed Oct 29 15:32:58 2008 +0100
     1.2 +++ b/NEWS	Thu Oct 30 10:57:45 2008 +0100
     1.3 @@ -77,6 +77,19 @@
     1.4  * Global versions of theorems stemming from classes do not carry
     1.5  a parameter prefix any longer.  INCOMPATIBILITY.
     1.6  
     1.7 +* Dropped locale element "includes".  This is a major INCOMPATIBILITY.
     1.8 +In existing theorem specifications replace the includes element by the
     1.9 +respective context elements of the included locale, omitting those that
    1.10 +are already present in the theorem specification.  Multiple assume
    1.11 +elements of a locale should be replaced by a single one involving the
    1.12 +locale predicate.  In the proof body, declarations (most notably
    1.13 +theorems) may be regained by interpreting the respective locales in the
    1.14 +proof context as required (command "interpret").
    1.15 +If using "includes" in replacement of a target solely because the
    1.16 +parameter types in the theorem are not as general as in the target,
    1.17 +consider declaring a new locale with additional type constraints on the
    1.18 +parameters (context element "constrains").
    1.19 +
    1.20  * Dropped "locale (open)".  INCOMPATBILITY.
    1.21  
    1.22  * Interpretation commands no longer attempt to simplify goal.