The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

Hi

I'm glad to announce a short but interesting new user contribution by
Stefan Berghofer. It is a formalization of the Coquand & Friedlender
constructive proof of Higman's lemma for a two-letter alphabet.

This Coq contribution is actually a translation by Stefan of his
original formalization in Isabelle made during his PhD.

Until the next Coq release, the files of this contribution can only be
retreived via Coq anonymous CVS. To get them, you just have to run the 2
following commands:
_________________________________________________________________________________
cvs -d 
:pserver:anoncvs AT coqcvs.inria.fr:/coq
 login
 <just press enter as passwd>
cvs -z3 -d 
:pserver:anoncvs AT coqcvs.inria.fr:/coq
 checkout contrib/Muenchen/Higman
________________________________________________________________________________

To compile, you need a not-too-old CVS version of Coq. More informations
can be found in the README, in particular how to use the program extracted
from the Coq proofs.

Pierre Letouzey

PS: to contact the author:

        Stefan Berghofer
        E-Mail: 
berghofe AT in.tum.de
        Web: http://www.in.tum.de/~berghofe