Email Gateway (Aug 22 2022 at 18:56): Email Gateway (Aug 22 2022 at 18:56):From: noam neer <noamneer@gmail.com>
hi everybody.
I tried to prove a simple lemma using sledgehammer (on Isabelle 2018.)
I got back a long "metis" command.
I pasted it in my code, and it got colored purple.
As far as I remember, this color means that the system is still running
without success.
However when I put the marker after the lemma, the output (in the lower
window)
shows that the theorem was proved successfully and can be used.
So, was it proved or not?
thanx
(a text file with the code itself is attached.)
[image: query_19_01_15.png]
query_19_01_15.png
query_19_01_15.thy
Email Gateway (Aug 22 2022 at 18:56):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Noam,
As far as I can tell: it was not.
As long as you have a purple command, proofs are not really finished,
but nevertheless (to facilitate parallel checking among other things)
the corresponding results are already available for later proofs.
Isabelle/jEdit is great for interactive development, but in my own
proofs I always use "isabelle build" in the end to make sure that
everything actually runs through.
hope this helps,
chris
Last updated: Apr 25 2024 at 16:19 UTC