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
Hi
It's always problematic if the user cannot be sure whether his theorem
is actually proved, or the proof method is just diverging in a parallel
thread. Thus, a UI should provide very clear information to the user,
otherwise we will get Problem reports of the form: Everything runs
fine in JEdit,