NEWS
changeset 30964 e80c06577ade
parent 30957 20d01210b9b1
child 30965 e0938d929bfd
--- a/NEWS	Wed Apr 22 19:09:25 2009 +0200
+++ b/NEWS	Wed Apr 22 19:12:15 2009 +0200
@@ -23,6 +23,11 @@
     relpow with infix syntax "^^"
     funpow with infix syntax "^o"
 
+  Power operations on algebraic structures retains syntax "^" and is now defined
+  generic in class recpower; class power disappeared.  INCOMPATIBILITY.
+
+* ML antiquotation @{code_datatype} inserts definition of a datatype generated
+by the code generator; see Predicate.thy for an example.
 
 
 New in Isabelle2009 (April 2009)