[isabelle-dev] Checked "assume" command

[Lars Noschinski]

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