[isabelle-dev] Checked "assume" command
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
> 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