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

[Alexander Krauss]

Makarius wrote:
> On Wed, 9 Feb 2011, Tobias Nipkow wrote:
> 
>>>> 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.
> 

[...]
> I can't give a comprehensive overview right 
> now, apart from what is written in the implementation manual.  (How many 
> people have actually read it?)

I have read it (just for the records), but I think the comprehensive 
answer-to-everything is an answer to a different question...

> There are many more fine points that have shown up and been adressed 
> concerning the delicate question of contexts, variable scoping, renaming 
> etc. over years.  The discussion right now seems to say: This has all 
> been nonsense, and should be thrown away.

I don't think that anybody wants to say (or imply) anything like that. 
As I understood it, this particular point ("Why do nonzero indexnames 
show up in this situation, and shouldn't they rather be normalized to 
zero as they are in other situations (e.g. toplevel statements), too?") 
may simply be yet another fine point that one might want to address in 
the future.

In particular, this fine point is completely orthogonal to the issue of 
concrete syntax for indexnames that was raised initially.

Alex