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)