[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
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