--- 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 \\<forall>. 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 ***