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

[isabelle-dev] NEWS: isabelle.select-entity

*** Prover IDE -- Isabelle/Scala/jEdit *** * Action "isabelle.select-entity" (shortcut CS+ENTER) selects all occurences of the formal entity at the caret position. This facilitates systematic renaming. This refers to Isabelle/48bc9045866e. As usual, new keyboard shortcuts need to be provided