Re: [isabelle] Expansion of let-bindings in proofs



Hi Lars,

> 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.

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.

Jasmin





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