diff r d58d6acab331 r 398c0f48a99e NEWS
 a/NEWS Wed Jun 10 11:31:26 2009 +0200
+++ b/NEWS Wed Jun 10 11:31:36 2009 +0200
@@ 4,28 +4,38 @@
New in this Isabelle version

+*** General ***
+
+* Discontinued old form of "escaped symbols" such as \\. Only
+one backslash should be used, even in ML sources.
+
+
*** Pure ***
* On instantiation of classes, remaining undefined class parameters are
formally declared. INCOMPATIBILITY.
+* On instantiation of classes, remaining undefined class parameters
+are formally declared. INCOMPATIBILITY.
*** HOL ***
* 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 operations on relations and functions are now one dedicate constant compow with
infix syntax "^^". Power operations on multiplicative monoids retains syntax "^"
and is now defined generic in class power. INCOMPATIBILITY.

* ML antiquotation @{code_datatype} inserts definition of a datatype generated
by the code generator; see Predicate.thy for an example.

* New method "linarith" invokes existing linear arithmetic decision procedure only.
+* 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 operations on relations and functions are now one dedicate
+constant compow with infix syntax "^^". Power operations on
+multiplicative monoids retains syntax "^" and is now defined generic
+in class power. INCOMPATIBILITY.
+
+* ML antiquotation @{code_datatype} inserts definition of a datatype
+generated by the code generator; see Predicate.thy for an example.
+
+* New method "linarith" invokes existing linear arithmetic decision
+procedure only.
*** ML ***