author | wenzelm |
Fri, 27 Sep 2024 14:22:06 +0200 | |
changeset 80971 | 2c57002d98e4 |
parent 80970 | 74ba8ec496c1 |
child 80972 | 7c1e73540990 |
--- a/src/Pure/library.ML Fri Sep 27 13:52:16 2024 +0200 +++ b/src/Pure/library.ML Fri Sep 27 14:22:06 2024 +0200 @@ -626,11 +626,11 @@ (* lists of integers *) -(*make the list [from, from + 1, ..., to]*) +(*make the list [i, i + 1, ..., j]*) fun ((i: int) upto j) = if i > j then [] else i :: (i + 1 upto j); -(*make the list [from, from - 1, ..., to]*) +(*make the list [i, i - 1, ..., j]*) fun ((i: int) downto j) = if i < j then [] else i :: (i - 1 downto j);