[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


Attachment: Thesis.thy
Description: Binary data

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