# 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);