# HG changeset patch
# User haftmann
# Date 1240420335 -7200
# Node ID e80c06577ade75b4aa589ba48c3fa1570a19c213
# Parent  f44736b9d804b748f24162bfd8fe8e1c3c79b339
code_datatype and power

diff -r f44736b9d804 -r e80c06577ade NEWS
--- 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)