Verification of the Redecoration Algorithm for Triangular Matrices

Proof scripts that were working in 2007 on the then current releases of Coq and Isabelle

Added in late 2010

Added in late 2012

A version with tiny modifications to run in version 8.4 of Coq (tested with 8.4pl1 in December 2012):
Ralph Matthes
Last modified: Fri Dec 28 16:02:21 CET 2012