[isabelle-dev] Checked "assume" command
noschinl at in.tum.de
Wed Sep 5 15:00:50 CEST 2012
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"
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.
More information about the isabelle-dev