Re: [isabelle-dev] Whole word search

On 07/06/16 10:10, Fabian Immler wrote: > >> Am 06.06.2016 um 21:29 schrieb Makarius : >> >> It means that the parts of long identifiers can be selected individually >> (e.g. via double-clicked). It also has an effect on searching "x" in >> "x.", but note that the lambda in

Re: [isabelle-dev] Whole word search

On 06/06/16 22:40, Lawrence Paulson wrote: >> On 6 Jun 2016, at 20:29, Makarius wrote: >> >> >> Anyway, for the described application to rename the "x" within a lambda >> expression, you can now use isabelle.select-entity as described in >>

Re: [isabelle-dev] Whole word search

But what is the scope of this selection? The entire file or some local scope? Larry > On 6 Jun 2016, at 20:29, Makarius wrote: > > > Anyway, for the described application to rename the "x" within a lambda > expression, you can now use isabelle.select-entity as described in

Re: [isabelle-dev] Whole word search

On 27/05/16 17:53, Lawrence Paulson wrote: > There appear to have been some changes in policy concerning the meaning of > “whole word” in jEdit find and replace. Let’s suppose that we want to rename > the variable x in the expression λx. if P x then 1 else 0. For quite some > time, the