Am 17/08/2013 15:24, schrieb Makarius: > On Thu, 15 Aug 2013, Lawrence Paulson wrote: > >> On 13 Aug 2013, at 10:35, Lars Noschinski <nosch...@in.tum.de> wrote: >>> >>> It might be interesting to note that also Unify.matchers is not able to >>> match >>> such term. > > This old thread on Unify.matchers might be also interesting: > https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-August/msg00080.html >
The relationship is rather tenuous. That old thread is not about an incompleteness but merely about the eta-expansion of the result. Tobias > Makarius > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
