But what is the scope of this selection? The entire file or some local scope? Larry
> 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 > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev