| changeset 24643 | d5e4b170d132 |
| parent 24636 | e758837c0d18 |
| child 24649 | f7b68d12a91e |
--- 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