On 02/09/2011 03:39 PM, Tobias Nipkow wrote:
If your analogy with lambda calculus is correct, than there are
situations when one must rename something exported from a proof block.
That I do not understand. Take this example:
lemma True
proof-
{ fix n::nat have "n=n" by auto }
produces "?n2 = ?n2". I do not see why it could not produce ?n = ?n.
AFAIK this question is mostly equivalent to the question
"Why does Variable.export use maxidx instead of reusing names and
relying on an invariant like 'names are always fixed'?"
and the answer I was given (by Makarius in May 2010 in private Email
conversation)
to that question is something like
"tools aren't this well behaved, such an invariant does not hold in
general."
IIRC I even had the pleasure to witness this behaviour in actual code.
Regards,
Andy
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
