[isabelle-dev] Checked "assume" command

[Lawrence Paulson]

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.

Larry

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.