Historically, the point is that index numbers were regarded as very important in variable names, while identifiers ending with digits were not seen as important. And there are other ways of making multiple identifiers. Nowadays, there aren't that many situations where a user would need to refer to a nonzero index number. Larry
On 8 Feb 2011, at 16:24, Tobias Nipkow wrote: > I don't mind one way or the other, but also wonder if it is worth it - I > will certainly not rush in to change it. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
