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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
