changeset 10726 | e12b81140945 |
parent 10664 | da5373fa06de |
child 10756 | 831c864cc56e |
--- a/NEWS Fri Dec 22 13:53:28 2000 +0100 +++ b/NEWS Fri Dec 22 18:20:55 2000 +0100 @@ -72,7 +72,8 @@ (as While_Combinator), HOL/Lex/Prefix (as List_Prefix); * HOL basics: added overloaded operations "inverse" and "divide" -(infix "/"), syntax for generic "abs" operation; +(infix "/"), syntax for generic "abs" operation, generic summation +operator; * HOL/typedef: simplified package, provide more useful rules (see also HOL/subset.thy);