[isabelle-dev] find_theorems raises UnequalLengths exception

Makarius 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 mailing list