Hi all, I want to have an Isabelle/ML function that takes a theorem and completely eta-reduces all the terms in its conclusion. Is there an idiomatic way to do this? I'm still trying to get this working after over a day of "looking up the Isabelle 'documentation'".

IIRC eta reduction is done automatically when constructing theorems (but I don’t have Isabelle to test it right now).

It "usually" is, but methods (e.g. induction, and maybe the simplifier?) sometimes eta-expand in the middle of a proof and I need the eta-normalized form again.

I've figured it out using conversions and other bits from Thm.ML.

Last updated: Aug 15 2022 at 04:16 UTC