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

[Tobias Nipkow]

Having to instantiate an indexed ?-variable can require a bit of
experimentation if you don't remember the exact syntax. I am all for an
improvement here, and as Gerwin pointed out, one of our flagship
projects is using apply's heavily, where it probably comes up more
frequently than otherwise.

Tobias

Tjark Weber schrieb:
> 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
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev