[isabelle-dev] Checked "assume" command

Lars Noschinski 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"
   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 mailing list