| changeset 15044 | f224d27bb1f8 |
| parent 15033 | 255bc508a756 |
| child 15046 | d6a4c3992e9d |
--- a/NEWS Wed Jul 14 10:25:21 2004 +0200 +++ b/NEWS Thu Jul 15 08:38:37 2004 +0200 @@ -152,6 +152,8 @@ Moreover, the mathematically important symbolic identifier \<epsilon> becomes available as variable, constant etc. +* HOL: Summation over nat with syntax '\<Sum>i<k. e' is now just a + translation into 'setsum'. *** HOLCF ***