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

[Lawrence Paulson]

I'm only talking about cases where “show" must inevitably fail. Fortunately, such situations are rare, but if they can easily be detected, they should be.
Larry

On 5 Sep 2012, at 14:20, Lars Noschinski <noschinl at in.tum.de> wrote:

> 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