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

Andreas Schropp schropp at in.tum.de
Wed Feb 9 16:12:06 CET 2011

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 
to that question is something like
   "tools aren't this well behaved, such an invariant does not hold in 

IIRC I even had the pleasure to witness this behaviour in actual code.


More information about the isabelle-dev mailing list