No subject

[Thomas Forster]

My colleage Larry Paulson here in Cambridge has recently 
formalized the consistency proof for AC (Goedel's constructible universe, etc.) using Isabelle/ZF. A short note on this  proof is here:

 http://www.cl.cam.ac.uk/users/lcp/papers/Sets/constructible-abs.pdf

 A document automatically generated from the proof is here (beware, 281 
 pages!):

 http://www.cl.cam.ac.uk/users/lcp/papers/Sets/constructible-theory.pdf