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

[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


 	Makarius