1.1 --- a/NEWS	Fri Dec 22 13:53:28 2000 +0100
     1.2 +++ b/NEWS	Fri Dec 22 18:20:55 2000 +0100
     1.3 @@ -72,7 +72,8 @@
     1.4  (as While_Combinator), HOL/Lex/Prefix (as List_Prefix);
     1.5  
     1.6  * HOL basics: added overloaded operations "inverse" and "divide"
     1.7 -(infix "/"), syntax for generic "abs" operation;
     1.8 +(infix "/"), syntax for generic "abs" operation, generic summation
     1.9 +operator;
    1.10  
    1.11  * HOL/typedef: simplified package, provide more useful rules (see also
    1.12  HOL/subset.thy);