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

[Tobias Nipkow]

>> It is interesting that local scopes within structured proofs generate
>> theorems with nonzero indices, but of course that is a separate matter.
> 
> Yes, that is a new aspect that was introduced around 1998/1999.

I would be more interested in the why than the when. Generating
unpredictable names does not contribute to stability of proofs.

Tobias