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

[Jasmin Christian Blanchette]

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.

Jasmin