summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

NEWS

changeset 31547 | 398c0f48a99e |

parent 31481 | 60ae1588f232 |

child 31626 | fe35b72b9ef0 |

--- 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 ***