Index of /ports/math/isabelle/work/Isabelle/src/ZF/AC

 Name                    Last modified       Size  Description

 Parent Directory        09-Aug-2008 06:10      -  
 AC15_WO6.thy            17-Jun-2005 07:15    11k  
 AC15_WO6.thy.html       09-Aug-2008 06:10     0k  
 AC16_WO4.thy            17-Jun-2005 07:15    23k  
 AC16_WO4.thy.html       09-Aug-2008 06:10     0k  
 AC16_lemmas.thy         17-Jun-2005 07:15     9k  
 AC16_lemmas.thy.html    09-Aug-2008 06:10     0k  
 AC17_AC1.thy            17-Jun-2005 07:15    10k  
 AC17_AC1.thy.html       09-Aug-2008 06:10     0k  
 AC18_AC19.thy           17-Jun-2005 07:15     3k  
 AC18_AC19.thy.html      09-Aug-2008 06:10     0k  
 AC7_AC9.thy             17-Jun-2005 07:15     7k  
 AC7_AC9.thy.html        09-Aug-2008 06:10     0k  
 AC_Equiv.thy            17-Jun-2005 07:15     9k  
 AC_Equiv.thy.html       09-Aug-2008 06:10     0k  
 Cardinal_aux.thy        17-Jun-2005 07:15     8k  
 Cardinal_aux.thy.html   09-Aug-2008 06:10     0k  
 DC.thy                  17-Jun-2005 07:15    23k  
 DC.thy.html             09-Aug-2008 06:10     0k  
 HH.thy                  17-Jun-2005 07:15     9k  
 HH.thy.html             09-Aug-2008 06:10     0k  
 Hartog.thy              17-Jun-2005 07:15     3k  
 Hartog.thy.html         09-Aug-2008 06:10     0k  
 ROOT.ML                 16-Jan-2002 08:52     1k  
 ROOT.ML.html            09-Aug-2008 06:10     0k  
 WO1_AC.thy              17-Jun-2005 07:15     4k  
 WO1_AC.thy.html         09-Aug-2008 06:10     0k  
 WO1_WO7.thy             17-Jun-2005 07:15     4k  
 WO1_WO7.thy.html        09-Aug-2008 06:10     0k  
 WO2_AC16.thy            17-Jun-2005 07:15    23k  
 WO2_AC16.thy.html       09-Aug-2008 06:10     0k  
 WO6_WO1.thy             17-Jun-2005 07:15    22k  
 WO6_WO1.thy.html        09-Aug-2008 06:10     0k  
 document/               09-Aug-2008 06:10      -  

AC -- Equivalents of the Axiom of Choice

@book{rubin&rubin,
  author	= "Herman Rubin and Jean E. Rubin",
  title		= "Equivalents of the Axiom of Choice, {II}",
  publisher	= "North-Holland",
  year		= 1985}

The report Mechanizing Set Theory, by Paulson and Grabczewski, describes both this development and ZF's theories of cardinals.