--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/README.html	Tue Mar 05 16:50:17 1996 +0100
@@ -0,0 +1,24 @@
+<!-- $Id$ -->
+<HTML><HEAD><TITLE>HOL/AC</TITLE></HEAD><BODY>
+
+<H2>AC -- Equivalents of the Axiom of Choice</H2>
+
+Krzysztof Grabczewski has mechanized the first two chapters of the book
+
+<P>
+<PRE>
+@book{rubin&rubin,
+  author	= "Herman Rubin and Jean E. Rubin",
+  title		= "Equivalents of the Axiom of Choice, {II}",
+  publisher	= "North-Holland",
+  year		= 1985}
+</PRE>
+
+<P>
+The report
+<A HREF="http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz">Mechanizing Set Theory</A>, by Paulson and Grabczewski, describes both this development and ZF's theories of cardinals.
+<P>
+
+<HR>
+
+<P>Last modified 5 March 1996