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

Hi Jasmin,

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

thanks for the investigation. Apparently spontaneous eta-contraction is a
tricky business. I just wonder why the 'induction' method appears to
eta-expand terms occurring in my goal.


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