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

NEWS

changeset 23377 | 197b6a39592c |

parent 23369 | 227c51012cdb |

child 23379 | d0e3f790bd73 |

--- a/NEWS Wed Jun 13 18:30:17 2007 +0200 +++ b/NEWS Wed Jun 13 19:14:51 2007 +0200 @@ -546,6 +546,12 @@ *** HOL *** +* IntDef: The constant "int :: nat => int" has been removed; now + "int" is an abbreviation for "of_nat :: nat => int". Potential + INCOMPATIBILITY due to differences in default simp rules: + - "int (Suc m)" simplifies to "int m + 1" instead of "1 + int m" + - "int (m * n)" simplifies to "int m * int n" + * Method "algebra" solves polynomial equations over (semi)rings using Groebner bases. The (semi)ring structure is defined by locales and the tool setup depends on that generic context. Installing the