Re: [isabelle] Expansion of let-bindings in proofs
> 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