On Thu, 2012-11-08 at 12:41 +0100, Jasmin Christian Blanchette wrote: > Actually, Z3 fails to refind the proof on my machine. Perhaps I'm using > a different version of Z3 than Ondrej used. So I've now delegated the > issue to Ondrej, who's more likely to be able to refind the proofs that > he found once.
I've had the same experience before, while exchanging theories that heavily relied on sledgehammer with other people across different machines and prover versions: re-finding proofs is a brittle process. I am not sure whether that is an argument in favor of certificates, or what the best solution would be. Best regards, Tjark _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
