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

[Tobias Nipkow]

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
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>