[isabelle-dev] find_theorems raises UnequalLengths exception
makarius at sketis.net
Fri Nov 19 15:17:45 CET 2010
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.
More information about the isabelle-dev