[isabelle-dev] Checked "assume" command
lp15 at cam.ac.uk
Wed Sep 5 14:48:06 CEST 2012
Something of this general sort would certainly be useful. Having the wrong assumption is the most insidious of errors. The only similar one is misusing "fix". It would be great to be told when your context is wrong.
On 5 Sep 2012, at 13:45, Lars Noschinski <noschinl at in.tum.de> wrote:
> Also, this change gives an fail-early property, which is useful when maintaining proofs.
More information about the isabelle-dev