--- a/src/ZF/Constructible/README.html Tue Mar 12 19:55:17 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<html>
-
-<head>
- <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
- <title>ZF/Constructible/README</title>
-</head>
-
-<body>
-<h1>Constructible--Relative Consistency of the Axiom of Choice</h1>
-
-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>