tuned;

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