# HG changeset patch
# User haftmann
# Date 1240213936 -7200
# Node ID ef2319d6b6a55d04f0c70631cb3517c90a995127
# Parent  cf50e67bc1d1b351a8ea2b21c66b9b7057095fb6
changes in power operations

diff -r cf50e67bc1d1 -r ef2319d6b6a5 NEWS
--- a/NEWS	Mon Apr 20 09:32:40 2009 +0200
+++ b/NEWS	Mon Apr 20 09:52:16 2009 +0200
@@ -9,14 +9,18 @@
 
 *** HOL ***
 
-* Class semiring_div now requires no_zero_divisors and proof of div_mult_mult1;
+* Class semiring_div requires superclass no_zero_divisors and proof of div_mult_mult1;
 theorems div_mult_mult1, div_mult_mult2, div_mult_mult1_if, div_mult_mult1 and
 div_mult_mult2 have been generalized to class semiring_div, subsuming former
 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.
+* Power operations on relations and functions are now dedicated constants:
+
+    relpow with infix syntax "^^"
+    funpow with infix syntax "^o"
+
+INCOMPATIBILITY.
 
 New in Isabelle2009 (April 2009)
 --------------------------------