changed simp rules for of_nat
authorhuffman
Thu Jun 21 22:30:58 2007 +0200 (2007-06-21)
changeset 23468d27d79a47592
parent 23467 d1b97708d5eb
child 23469 3f309f885d0b
changed simp rules for of_nat
NEWS
     1.1 --- a/NEWS	Thu Jun 21 22:10:16 2007 +0200
     1.2 +++ b/NEWS	Thu Jun 21 22:30:58 2007 +0200
     1.3 @@ -548,11 +548,12 @@
     1.4    It generates calls to the "metis" method if successful. These can be pasted into the proof.
     1.5    Users do not have to wait for the automatic provers to return.
     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 +* IntDef: The constant "int :: nat => int" has been removed; now "int"
    1.13 +  is an abbreviation for "of_nat :: nat => int". The simplification rules
    1.14 +  for "of_nat" have been changed to work like "int" did previously.
    1.15 +  (potential INCOMPATIBILITY)
    1.16 +  - "of_nat (Suc m)" simplifies to "1 + of_nat m" instead of "of_nat m + 1"
    1.17 +  - of_nat_diff and of_nat_mult are no longer default simp rules
    1.18  
    1.19  * Method "algebra" solves polynomial equations over (semi)rings using
    1.20    Groebner bases. The (semi)ring structure is defined by locales and