[isabelle] New error messages in Isabelle 2013



Dear Isabelle Users,

Maybe it is just me, but I still get confused by the new error messages in
Isabelle 2013. Of course, it is already
a big improvement over simply "failed to finish proof" from Isabelle 2012.

For instance, the success of establishing a "have" or a "show" is usually
show in the output window
with a message like "have fact"  " show fact ... successful attempt to
solve goal by exported rule"

Now, when there´s a failure, the error message is still prefixed in the
output window by the
very messages we get when we are successful, as mentioned above. Besides in
the error case, the
output window also show after the error message that there are no subgoals
(?).

 I attach two images to make my point clearer.
In this particular example, if the error message was not prefixed by
"Successful attempt ...", I think it would
be much better.

Is my confusion justified?

Best!
-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil

Attachment: jedit-proof-sucess.PNG
Description: PNG image

Attachment: jedit-proof-failure.PNG
Description: PNG image



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