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