[isabelle] finished proof contains coloured proof method



Hi,

at the last section of a proof Isabelle/jEdit show the last proof method in colour, see the attachment. According to

http://stackoverflow.com/questions/22635300/what-do-colour-codes-mean-in-isabelle-jedit

the purple colour means that a prover process is still running.

Despite of this, I can finish the proof by qed and I get

theorem    (?Xs::form list)     â  (?P::form)     â âYs::form list.    Ys    cfâ ?P

Is this a valid proof? Can I simply ignore this colouring?

I use vanilla Isabelle2016.

- Gergely

Attachment: cutfree.error.PNG
Description: cutfree.error.PNG



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.