# HG changeset patch
# User wenzelm
# Date 977505655 -3600
# Node ID e12b81140945a67a77e9101a803315ccf49f6289
# Parent  ea048ad152837389d7ce445ba2013f305679ffa6
tuned;

diff -r ea048ad15283 -r e12b81140945 NEWS
--- 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);