# HG changeset patch
# User nipkow
# Date 904908250 -7200
# Node ID 5a6c4f666a2549b376e37ed6c8d9f1c01d122a8d
# Parent  26c9a7c0b36b213be52052ec26eed9a2d9b54551
Function 'upt'

diff -r 26c9a7c0b36b -r 5a6c4f666a25 NEWS
--- 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: