On 06/06/16 22:40, Lawrence Paulson wrote:
>> On 6 Jun 2016, at 20:29, Makarius <makar...@sketis.net> wrote:
>>
>>
>> Anyway, for the described application to rename the "x" within a lambda
>> expression, you can now use isabelle.select-entity as described in
>> https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2016-June/006879.html
> But what is the scope of this selection? The entire file or some local scope?
It is the true scope of the lambda term -- assuming that it has been
formally checked by the prover.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
