[isabelle-dev] [OT] Checked "assume" command
noschinl at in.tum.de
Wed Sep 5 15:20:00 CEST 2012
On 05.09.2012 15:13, Lawrence Paulson wrote:
> Fixing a variable that ought to be free is an error.
> Highlighting is useful, but you have to be quite alert to notice it. I seldom notice it except in really blatant situations, like the same variable highlighted in two different ways. If the context is simply wrong, the highlighting should be absolutely unmissable.
Indeed, a variable shadowed by mistake is quite hard to detect. But is
there a clear rule whether a variable "ought to be free"? Shadowing has
its legitimate use cases (e.g. I usually shadow the "n" in induction
proofs on the naturals).
More information about the isabelle-dev