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...
Tobias 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 _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
