NEWS
changeset 10514 3db037155f0e
parent 10474 25caae39bd7a
child 10547 efaba354b7f1
     1.1 --- a/NEWS	Thu Nov 23 16:25:08 2000 +0100
     1.2 +++ b/NEWS	Thu Nov 23 21:29:35 2000 +0100
     1.3 @@ -58,7 +58,8 @@
     1.4  HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While
     1.5  (as While_Combinator), HOL/Lex/Prefix (as List_Prefix);
     1.6  
     1.7 -* added overloaded operations "inverse" and "divide" (infix "/");
     1.8 +* HOL basics: added overloaded operations "inverse" and "divide"
     1.9 +(infix "/"), syntax for generic "abs" operation;
    1.10  
    1.11  * HOL/typedef: simplified package, provide more useful rules (see also
    1.12  HOL/subset.thy);