1.1 --- a/NEWS	Thu Oct 15 11:38:39 1998 +0200
     1.2 +++ b/NEWS	Thu Oct 15 12:15:14 1998 +0200
     1.3 @@ -193,6 +193,8 @@
     1.4  * reorganized the main HOL image: HOL/Integ and String loaded by
     1.5  default; theory Main includes everything;
     1.6  
     1.7 +* automatic simplification of integer sums and comparisons, using cancellation;
     1.8 +
     1.9  * added option_map_eq_Some and not_Some_eq to the default simpset and claset;
    1.10  
    1.11  * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset;