equal
deleted
inserted
replaced
|
1 <!-- $Id$ --> |
|
2 <HTML><HEAD><TITLE>HOL/AC</TITLE></HEAD><BODY> |
|
3 |
|
4 <H2>AC -- Equivalents of the Axiom of Choice</H2> |
|
5 |
|
6 Krzysztof Grabczewski has mechanized the first two chapters of the book |
|
7 |
|
8 <P> |
|
9 <PRE> |
|
10 @book{rubin&rubin, |
|
11 author = "Herman Rubin and Jean E. Rubin", |
|
12 title = "Equivalents of the Axiom of Choice, {II}", |
|
13 publisher = "North-Holland", |
|
14 year = 1985} |
|
15 </PRE> |
|
16 |
|
17 <P> |
|
18 The report |
|
19 <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. |
|
20 <P> |
|
21 |
|
22 <HR> |
|
23 |
|
24 <P>Last modified 5 March 1996 |