[isabelle] Expansion of let-bindings in proofs



Dear list,

as you all know, the 'proof' command introduces a let-binding "?thesis"
according to the preceding statement. I have observed a situation where
there is a difference between "?thesis" and the expanded term. See the
attached theory file. In the last proof step, if you replace the literal
term with "?thesis", the simplifier fails to solve the proposition.
However, both look completely identical. I have no idea what's going on
there.

Cheers
Lars

Attachment: Thesis.thy
Description: Binary data



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.