[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.
Jasmin
More information about the isabelle-dev
mailing list