[isabelle-dev] AFP: Session AVL-Trees broken

[Tjark Weber]

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