[isabelle-dev] Checked "assume" command

[Lawrence Paulson]

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.

Larry

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

> On 05.09.2012 14:54, Lawrence Paulson wrote:
>> Simply fixing too many or too few variables.
> 
> Fixing to many variables should not be a problem, i.e.
> 
>  lemma "!!n :: nat. n >= 0"
>  proof -
>    fix a b c
>    show "b >= 0" by auto
>  qed
> 
> works. In jEdit, the case of "too few fixed variables" is immediately obvious in most cases, because variables which are not in the context are highlighted differently.
> 
>  -- Lars