* HOL: syntax or "abs";
authorwenzelm
Thu Nov 23 21:29:35 2000 +0100 (2000-11-23)
changeset 105143db037155f0e
parent 10513 6be063dec835
child 10515 8430c8fa8a9f
* HOL: syntax or "abs";
NEWS
     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);