From this web site the files in which the work in the paper "Generating Certified Code from Formal Proofs: A Case Study in Homological Algebra" are available.
The files have been tested with the Isabelle 2008 distribution. They are built upon the HOL-Algebra logic.
Two different instances from the result known as "Basic Perturbation Lemma" (or BPL) are presented: