int abbreviates of_nat
authorhuffman
Wed Jun 13 19:14:51 2007 +0200 (2007-06-13)
changeset 23377197b6a39592c
parent 23376 53317a1ec8b2
child 23378 1d138d6bb461
int abbreviates of_nat
NEWS
     1.1 --- a/NEWS	Wed Jun 13 18:30:17 2007 +0200
     1.2 +++ b/NEWS	Wed Jun 13 19:14:51 2007 +0200
     1.3 @@ -546,6 +546,12 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* IntDef: The constant "int :: nat => int" has been removed; now
     1.8 +  "int" is an abbreviation for "of_nat :: nat => int". Potential
     1.9 +  INCOMPATIBILITY due to differences in default simp rules:
    1.10 +  - "int (Suc m)" simplifies to "int m + 1" instead of "1 + int m"
    1.11 +  - "int (m * n)" simplifies to "int m * int n"
    1.12 +
    1.13  * Method "algebra" solves polynomial equations over (semi)rings using
    1.14    Groebner bases. The (semi)ring structure is defined by locales and
    1.15    the tool setup depends on that generic context. Installing the