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

NEWS

changeset 5428 | 5a6c4f666a25 |

parent 5407 | b450fea6d70c |

child 5475 | 410172655d64 |

--- a/NEWS Fri Sep 04 11:01:59 1998 +0200 +++ b/NEWS Fri Sep 04 13:24:10 1998 +0200 @@ -216,6 +216,9 @@ * HOL/List: - new function list_update written xs[i:=v] that updates the i-th list position. May also be iterated as in xs[i:=a,j:=b,...]. + - new function `upt' written [i..j(] which generates the list + [i,i+1,...,j-1], i.e. the upper bound is excluded. To include the upper + bound write [i..j], which is a shorthand for [i..j+1(]. - new lexicographic orderings and corresponding wellfoundedness theorems. * HOL/Arith: