[isabelle-dev] find_theorems raises UnequalLengths exception

Tobias Nipkow nipkow at in.tum.de
Fri Nov 19 15:57:36 CET 2010

The idea was that that code would be incomplete but not incorrect
outside the HO pattern term language. But indeed, th actual code has not
been verified...


Makarius schrieb:
> 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

More information about the isabelle-dev mailing list