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 <[email protected]> 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
