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
