## AC -- Equivalents of the Axiom of Choice

Krzysztof Grabczewski has mechanized the first two chapters of the book

    @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.