# HG changeset patch
# User wenzelm
# Date 1190195407 -7200
# Node ID d5e4b170d13241dd905b5172211e22916bcc072a
# Parent  7865c239ba081a94e9df25f2b4c19183a85eb9e9
* ML: just one true type int;

diff -r 7865c239ba08 -r d5e4b170d132 NEWS
--- a/NEWS	Tue Sep 18 18:53:55 2007 +0200
+++ b/NEWS	Wed Sep 19 11:50:07 2007 +0200
@@ -1152,6 +1152,9 @@
 
 *** ML ***
 
+* ML basics: just one true type int, which coincides with IntInf.int
+(even on SML/NJ).
+
 * Generic arithmetic modules: Tools/rat.ML, Tools/float.ML
 
 * Context data interfaces (Theory/Proof/GenericDataFun): removed