[isabelle-dev] [isabelle] match_tac, schematic and bound variables
nipkow at in.tum.de
Mon Aug 19 08:26:29 CEST 2013
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:
The relationship is rather tenuous. That old thread is not about an
incompleteness but merely about the eta-expansion of the result.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev