Re: [isabelle-dev] superfluous [?]

2012-10-10 Thread Makarius
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

Re: [isabelle-dev] superfluous [?]

2012-10-10 Thread Peter Lammich
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,