* HOL: syntax or "abs";

--- a/NEWS	Thu Nov 23 16:25:08 2000 +0100
+++ b/NEWS	Thu Nov 23 21:29:35 2000 +0100
@@ -58,7 +58,8 @@
 HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While
 (as While_Combinator), HOL/Lex/Prefix (as List_Prefix);
 
-* added overloaded operations "inverse" and "divide" (infix "/");
+* HOL basics: added overloaded operations "inverse" and "divide"
+(infix "/"), syntax for generic "abs" operation;
 
 * HOL/typedef: simplified package, provide more useful rules (see also
 HOL/subset.thy);