--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/README.html Mon May 12 12:36:22 2003 +0200
@@ -0,0 +1,28 @@
+<HTML><HEAD><TITLE>ZF/Constructible/README</TITLE></HEAD><BODY>
+
+<H1>Constructible--Relative Consistency of the Axiom of Choice</H1>
+
+<P>Gödel's proof of the relative consistency of the axiom of choice is
+mechanized using Isabelle/ZF. The proof builds upon a previous mechanization
+of the
+<A HREF="http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf">reflection
+theorem</A>. The heavy reliance on metatheory in the original proof makes the
+formalization unusually long, and not entirely satisfactory: two parts of the
+proof do not fit together. It seems impossible to solve these problems
+without formalizing the metatheory. However, the present development follows
+a standard textbook, Kunen's <STRONG>Set Theory</STRONG> and could support the
+formalization of further material from that book. It also serves as an
+example of what to expect when deep mathematics is formalized.
+
+A paper describing this development is
+<A HREF="http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf">available</A>.
+
+<HR>
+<P>Last modified $Date$
+
+<ADDRESS>
+<A
+HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
+<A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
+</ADDRESS>
+</BODY></HTML>
\ No newline at end of file