author | nipkow |

Fri Sep 04 13:24:10 1998 +0200 (1998-09-04) | |

changeset 5428 | 5a6c4f666a25 |

parent 5427 | 26c9a7c0b36b |

child 5429 | 0833486c23ce |

Function 'upt'

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: