# HG changeset patch
# User wenzelm
# Date 975011375 -3600
# Node ID 3db037155f0efe0a0341ba2873fbfbc761e8e3a2
# Parent  6be063dec8353a7f86f93294014f708c2b3ca868
* HOL: syntax or "abs";

diff -r 6be063dec835 -r 3db037155f0e NEWS
--- 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);