[isabelle-dev] superfluous [?]
makarius at sketis.net
Wed Oct 10 17:52:56 CEST 2012
On Wed, 10 Oct 2012, Ondřej Kunčar wrote:
> This problem refers to 3fc6b3289c31.
> If I type in this simple formalization
> lemma c: "x = x"
> by metis
> thm c
> the following theorem is printed "?x = ?x [?]". What is that suspicious
> question mark? It seems to be produced by any metis call. And it is
> reproducible almost always.
This is the normal result of printing Thm.status_of in the traditional
way. It is now getting in the way, because terminal proofs ('by') are
always parallel in Isabelle/jEdit.
I am about to rework this critical kernal status information, but it
requires some more thinking. Last time I changed something there, it was
immediately reported as "problem" that fewer [!] were printed as before.
More information about the isabelle-dev