[isabelle-dev] Feature suggestion: apply (meth[1!])

[Lawrence Paulson]

I can also imagine a use for this sort of thing. I use structured proofs when I can, but in some situations it really isn't possible.

Larry

On 11 Mar 2013, at 16:51, Makarius <makarius at sketis.net> wrote:

> This looks just like making the meaning of indentation a bit more formal. Lets say as a mode of checking in the Prover IDE: fail if something is wrong in that respect, or paint things in funny colors.
> 
> Markup.proof_state is there for a long time already, to turn it into some use.