diff -r 7f699568a877 -r 37f887b55e7f NEWS --- a/NEWS Fri Apr 17 15:14:06 2009 +0200 +++ b/NEWS Fri Apr 17 15:57:26 2009 +0200 @@ -9,6 +9,9 @@ theorems zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default. INCOMPATIBILITY. +* Power operation on relations and functions is now a dedicated overloaded constant +funpower with infix syntax "^^". INCOMPATIBILITY. + New in Isabelle2009 (April 2009) --------------------------------