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 <[email protected]> wrote: > Also, this change gives an fail-early property, which is useful when > maintaining proofs. _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
