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