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

[Tjark Weber]

On Tue, 2011-02-08 at 06:53 -0800, Brian Huffman wrote:
> Honestly, I think the above parsing rules are quite confusing, and
> should be changed. I instantiate variables in theorems quite often,
> and many theorems use variable names that end in digits, but I almost
> never need to refer to variables with indices other than 0.

For what it's worth, I agree with Brian here.  I remember that this was
one of the minor hurdles when I first encountered Isabelle -- the kind
of technicality that can take a new user anywhere from 5 minutes to
\infty to figure out.  Changing the current behavior in my humble
opinion would be an improvement.

Kind regards,
Tjark