[isabelle-dev] {..n} and {..<n}

[Tobias Nipkow]

On nat, the sets {0..n} and {..n} are the same, which can be irksome.
Hence I discourage the use of {..n}. However, there are notations such
as "SUM k<=n. t" which stand for "setsum (%k. t) {..n}" and introduce
{..n} by the backdoor.

I am tempted to get rid of this and related notations and restrict to
the canonical "SUM k=a..b. t".

Would anybody miss the "k<=n" variant?
Potential problem: for other types, eg int, k<=i cannot be replaced by
some "k=a..i". But "SUM k<=i", "UN k<=i" over int (let alone real) seem
unusual.

Feelings?

Tobias