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

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Mon Dec 3 11:19:45 CET 2012

Am 03.12.2012 um 11:02 schrieb Makarius:

> For Z3 in particular, there is also the problem that you have to be a non-commercial user to run it.  This is hypothetical at the moment, since there are no commercial Isabelle or AFP maintainers.

Incidentally, for AFP, Tobias's policy is that "smt" should not be used at all, because of the fragility of the certificates. For Isabelle itself, we should probably try to contain/reduce its use.


More information about the isabelle-dev mailing list