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

[Jasmin Christian Blanchette]

Am 08.11.2012 um 12:56 schrieb Lawrence Paulson:

> The long-term solution must be to deliver self-contained proof scripts, but obviously it will be difficult.

Indeed. The good news is that the DFG accepted Tobias's project proposal called "Hardening the Hammer", where the first item is about Isar proof reconstruction from ATP and SMT proofs. In the last couple of months, there has been progress on the ATP front already, thanks to Steffen Smolka. Once the ATP proofs are really polished, we'll attach the SMT proofs. To reconstruct proofs with theory reasoning, we would need to use existing Isabelle decision procedures (e.g., for linear arithmetic) and to develop dedicated proof methods (e.g., for algebraic datatypes).

Jasmin