[isabelle-dev] superfluous [?]

Ondřej Kunčar kuncar at in.tum.de
Wed Oct 10 17:47:01 CEST 2012


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.


More information about the isabelle-dev mailing list