[isabelle-dev] Whole word search

[Lawrence Paulson]

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 occurrence of x in “λx.” was not regarded as a “whole word”, but for a week or two recently, it was. I prefer the latter behaviour as being more consistent, even though I can see issues connected with compound identifiers. Is this topic worth discussing?

Larry