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