# HG changeset patch
# User huffman
# Date 1181754891 -7200
# Node ID 197b6a39592cc9bae6f4d362397af242520c2ab8
# Parent  53317a1ec8b2d456049f3d27c2afdf5c1c8b2972
int abbreviates of_nat

diff -r 53317a1ec8b2 -r 197b6a39592c NEWS
--- 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