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

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Thu Nov 8 11:55:10 CET 2012

Hi Gerwin,

Am 07.11.2012 um 22:41 schrieb Gerwin Klein:

> *** Bad certificate cache: missing certificate
> *** At command "by" (line 169 of "/mnt/nfsbroy/home/isatest/afp/devel/thys/AVL-Trees/AVL.thy")
> (real error)

OK, this is related to my Isabelle change 34b0464d7eef, which slightly affects the SMT problems generated (more specifically, it affects a comment in the SMT problems). This is enough to change the hasked key that's used to look up certificates. I hadn't realized that the "AVL-Trees" example also uses certificates. I'll regenerate them.

Sorry for the trouble.


More information about the isabelle-dev mailing list