[isabelle] AFP 2007

The Archive of Formal proofs has updated to Isabelle 2007.

All archive entries are fully tested and work with the new release, old versions of existing entries still remain available for download.

9 new entries have become accessible from the main page at

"Much Ado About Two" by Sascha Böhme

"Sums of Two and Four Squares" by Roelof Oosterhuis

"Fermat's Last Theorem for Exponents 3 and 4 and the Parameterisation of
Pythagorean Triples" by Roelof Oosterhuis

"POPLmark Challenge Via de Bruijn Indices" by Stefan Berghofer

"First-Order Logic According to Fitting" by Stefan Berghofer

"Fundamental Properties of Valuation Theory and Hensel's Lemma" by Hidetsune Kobayashi

"Hotel Key Card System" by Tobias Nipkow

"Abstract Hoare Logics" by Tobias Nipkow

"Flyspeck I: Tame Graphs" by Gertrud Bauer and Tobias Nipkow


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.