author | huffman |

Thu Jun 21 22:30:58 2007 +0200 (2007-06-21) | |

changeset 23468 | d27d79a47592 |

parent 23467 | d1b97708d5eb |

child 23469 | 3f309f885d0b |

changed simp rules for of_nat

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