[isabelle-dev] [OT] Checked "assume" command

Lawrence Paulson lp15 at cam.ac.uk
Thu Sep 6 16:02:24 CEST 2012

If it is unambiguously wrong, then the highlighting must be as bold as in the case of a syntax error. 

On 5 Sep 2012, at 14:35, Makarius <makarius at sketis.net> wrote:

> With the "case that must fail" we are getting back to the tendencies of this thread: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-May/002736.html
> where I failed to explain basic observations how warnings and errors get a slightly different meaning in the Prover IDE model.
> Concerning fixes (and implicit type abstractions) you know my basic plan already: highlight the situation in the source text in a way that tells the user what is there, and the user can then see by himself if it is what he had in mind or should have in mind.

More information about the isabelle-dev mailing list