NEWS
changeset 5428 5a6c4f666a25
parent 5407 b450fea6d70c
child 5475 410172655d64
     1.1 --- a/NEWS	Fri Sep 04 11:01:59 1998 +0200
     1.2 +++ b/NEWS	Fri Sep 04 13:24:10 1998 +0200
     1.3 @@ -216,6 +216,9 @@
     1.4  * HOL/List:
     1.5    - new function list_update written xs[i:=v] that updates the i-th
     1.6      list position. May also be iterated as in xs[i:=a,j:=b,...].
     1.7 +  - new function `upt' written [i..j(] which generates the list
     1.8 +    [i,i+1,...,j-1], i.e. the upper bound is excluded. To include the upper
     1.9 +    bound write [i..j], which is a shorthand for [i..j+1(].
    1.10    - new lexicographic orderings and corresponding wellfoundedness theorems.
    1.11  
    1.12  * HOL/Arith: