This is exactly why I am against SMT certificates in AFP entries. Ondrej, can you possibly remove them?
Tobias Am 08/11/2012 11:55, schrieb Jasmin Christian Blanchette: > 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 > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
