[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution

Lawrence Paulson lp15 at cam.ac.uk
Tue Feb 8 18:01:49 CET 2011


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.




More information about the isabelle-dev mailing list