Isabelle-FLP Refactored proofs from the AFP entry "A Constructive Proof for FLP" (eliminates almost 800 lines of proof). PDF document is at document/ouput.pdf