NEWS
changeset 30957 20d01210b9b1
parent 30904 cc6a6047a10f
parent 30955 ef2319d6b6a5
child 30964 e80c06577ade
     1.1 --- a/NEWS	Mon Apr 20 12:27:23 2009 +0200
     1.2 +++ b/NEWS	Mon Apr 20 16:28:13 2009 +0200
     1.3 @@ -4,6 +4,25 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** Pure ***
     1.8 +
     1.9 +* On instantiation of classes, remaining undefined class parameters are
    1.10 +formally declared.  INCOMPATIBILITY.
    1.11 +
    1.12 +
    1.13 +*** HOL ***
    1.14 +
    1.15 +* Class semiring_div requires superclass no_zero_divisors and proof of div_mult_mult1;
    1.16 +theorems div_mult_mult1, div_mult_mult2, div_mult_mult1_if, div_mult_mult1 and
    1.17 +div_mult_mult2 have been generalized to class semiring_div, subsuming former
    1.18 +theorems zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and zdiv_zmult_zmult2.
    1.19 +div_mult_mult1 is now [simp] by default.  INCOMPATIBILITY.
    1.20 +
    1.21 +* Power operations on relations and functions are now dedicated constants:
    1.22 +
    1.23 +    relpow with infix syntax "^^"
    1.24 +    funpow with infix syntax "^o"
    1.25 +
    1.26  
    1.27  
    1.28  New in Isabelle2009 (April 2009)