Re: [isabelle] Expansion of let-bindings in proofs
> 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
If you disable eta-contraction in printing, with
declare [[eta_contract = false]]
you will see that the two terms are not exactly the same, which is enough to derail the simplification.
This archive was generated by a fusion of
Pipermail (Mailman edition) and