NEWS
changeset 30949 37f887b55e7f
parent 30930 11010e5f18f0
child 30951 a6e26a248f03
     1.1 --- a/NEWS	Fri Apr 17 15:14:06 2009 +0200
     1.2 +++ b/NEWS	Fri Apr 17 15:57:26 2009 +0200
     1.3 @@ -9,6 +9,9 @@
     1.4  theorems zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and zdiv_zmult_zmult2.
     1.5  div_mult_mult1 is now [simp] by default.  INCOMPATIBILITY.
     1.6  
     1.7 +* Power operation on relations and functions is now a dedicated overloaded constant
     1.8 +funpower with infix syntax "^^".  INCOMPATIBILITY.
     1.9 +
    1.10  New in Isabelle2009 (April 2009)
    1.11  --------------------------------
    1.12