summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

NEWS

changeset 15046 | d6a4c3992e9d |

parent 15044 | f224d27bb1f8 |

child 15050 | e02f678887bb |

--- a/NEWS Thu Jul 15 13:11:34 2004 +0200 +++ b/NEWS Thu Jul 15 13:24:45 2004 +0200 @@ -152,8 +152,31 @@ 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'. +* HOL/SetInterval: The syntax for open intervals has changed: + + Old New + {..n(} -> {..<n} + {)n..} -> {n<..} + {m..n(} -> {m..<n} + {)m..n} -> {m<..n} + {)m..n(} -> {m<..<n} + + The old syntax is still supported but will disappear in the future. + For conversion use the following emacs search and replace patterns: + + {)\([^\.]*\)\.\. -> {\1<\.\.} + \.\.\([^(}]*\)(} -> \.\.<\1} + + They are not perfect but work quite well. + +* HOL: There is new syntax for summation over finite sets: + + '\<Sum>x | P. e' is the same as 'setsum (%x. e) {x. P}' + '\<Sum>x<k. e' is the same as 'setsum (%x. e) {..<k}' + + Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e' + now translates into 'setsum' as above. + *** HOLCF ***