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

Tobias Nipkow nipkow at in.tum.de
Wed Feb 9 14:22:28 CET 2011

>> 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.


More information about the isabelle-dev mailing list