Re: [isabelle] check phases
Am 30.07.2014 um 16:02 schrieb Lars Noschinski <noschinl at in.tum.de>:
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and