NEWS
changeset 60347 7d64ad9910e2
parent 60331 f215fd466e30
child 60352 d46de31a50c4
     1.1 --- a/NEWS	Mon Jun 01 18:59:20 2015 +0200
     1.2 +++ b/NEWS	Mon Jun 01 18:59:20 2015 +0200
     1.3 @@ -13,6 +13,17 @@
     1.4  (intermediate legacy feature in Isabelle2015).  INCOMPATIBILITY.
     1.5  
     1.6  
     1.7 +*** Pure ***
     1.8 +
     1.9 +* Abbreviations in type classes now carry proper sort constraint.
    1.10 +Rare INCOMPATIBILITY in situations where the previous misbehaviour
    1.11 +has been exploited previously.
    1.12 +
    1.13 +* Refinement of user-space type system in type classes: pseudo-local
    1.14 +operations behave more similar to abbreviations.  Potential
    1.15 +INCOMPATIBILITY in exotic situations.
    1.16 +
    1.17 +
    1.18  *** HOL ***
    1.19  
    1.20  * Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.