summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Thu, 15 Jul 2004 13:24:45 +0200 | |

changeset 15046 | d6a4c3992e9d |

parent 15045 | d59f7e2e18d3 |

child 15047 | fa62de5862b9 |

*** empty log message ***

--- 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 ***