CIV in Isabelle

Here is some information about work that I did towards the end of the summer of 2006. Later, I presented this is at a Galois technical seminar. The most interesting part of this page is the source code to the solution, which is best viewed via Isabelle's Proof General interface.