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

Makarius makarius at sketis.net
Sat Aug 17 15:24:24 CEST 2013

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: 


More information about the isabelle-dev mailing list