changeset 10514 | 3db037155f0e |
parent 10474 | 25caae39bd7a |
child 10547 | efaba354b7f1 |
--- 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);