[isabelle] Systematic renaming



Hi,

In Isabelle2016-1-RC2 the occurrences of P in "assumes" and "shows" are not highlighted and renamed:

theorem
  fixes P
  assumes P
  shows P
proof -
  show P using assms .
qed

theorem
  P
proof -
  show P sorry
qed

Relevant items in the NEWS file:

* Highlighting of entity def/ref positions wrt. cursor.

* Action "isabelle.select-entity" (shortcut CS+ENTER) selects all occurrences of the formal entity at the caret position. This facilitates systematic renaming.

Am I doing something wrong?

Thanks,

Jørgen




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.