[isabelle-dev] Beta/Eta normalisation and net matching.

[Tjark Weber]

On Wed, 2010-08-04 at 11:50 +1000, Thomas Sewell wrote:
> It occurs to me that I don't even know whether theorems in Isabelle
> can be assumed to be beta/eta normal. Does anyone have any quick
> pointers on that? Is there a potential bug here?

There are various pieces of code that expect terms and theorems to be in
some kind of normal form (e.g. beta-eta), and other pieces of code that
establish or preserve some kind of normal form.  These invariants are
often undocumented, and they have caused bugs more than once in the
past.

These bugs are not always trivial to hunt down either, because what you
see is not what you get: Isabelle performs (some) normalization upon
parsing/printing.

Tjark