On Fri, 19 Nov 2010, Tobias Nipkow wrote:
Just for the record: the code eta-expands terms on the fly, but the
presence of beta-redexes may well confuse it.
It is known for many years that the pattern unification does have
occasional problems with beta redexes. This is one of the things that
have never been touched so far because other problems might lurk in the
dark, and the whole thing is critical for the correctness of the kernel.
IIRC, I have discussed it with Stefan Berghofer the last time about 5
years, and he could not explain to me the exact situation.
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
