author | huffman |

Wed Jun 13 19:14:51 2007 +0200 (2007-06-13) | |

changeset 23377 | 197b6a39592c |

parent 23376 | 53317a1ec8b2 |

child 23378 | 1d138d6bb461 |

int abbreviates of_nat

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