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 _______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev