[isabelle-dev] [isabelle] match_tac, schematic and bound variables

[Tobias Nipkow]

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 <noschinl at 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev