[isabelle-dev] [OT] Checked "assume" command

[Lars Noschinski]

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).

   -- Lars