[isabelle-dev] Checked "assume" command

Lawrence Paulson lp15 at cam.ac.uk
Wed Sep 5 15:13:47 CEST 2012

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.


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

More information about the isabelle-dev mailing list