Re: [isabelle] check phases



Am 30.07.2014 um 16:02 schrieb Lars Noschinski <noschinl at in.tum.de>:

> Now,
> after checking the terms, I need to be able to associate the free
> variables which the right bound variables again. If I can expect the
> bound variables between root and HOLE to be the same before and after
> the check, this is easy.

I don't know if this will help with your application, but "Term.rename_abs" might be part of the solution.

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.