diff -r b05cd411d3d3 -r 2ff3a5589b05 src/ZF/README.html
--- a/src/ZF/README.html Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,84 +0,0 @@
-
-
-
-
-
-
- ZF/README
-
-
-
-
-ZF: Zermelo-Fraenkel Set Theory
-
-This directory contains the ML sources of the Isabelle system for
-ZF Set Theory, based on FOL.
-
-There are several subdirectories of examples:
-
-- AC
-
- subdirectory containing proofs from the book "Equivalents of the Axiom
-of Choice, II" by H. Rubin and J.E. Rubin, 1985. Thanks to Krzysztof
-Gr`abczewski.
-
-
- Coind
-
- subdirectory containing a large example of proof by co-induction. It
-is by Jacob Frost following a paper by Robin Milner and Mads Tofte.
-
-
- IMP
-
- subdirectory containing a semantics equivalence proof between
-operational and denotational definitions of a simple programming language.
-Thanks to Heiko Loetzbeyer & Robert Sandner.
-
-
- Resid
-
- subdirectory containing a proof of the Church-Rosser Theorem. It is
-by Ole Rasmussen, following the Coq proof by G�ard Huet.
-
-
- ex
-
- subdirectory containing various examples.
-
-
-Isabelle/ZF formalizes the greater part of elementary set theory,
-including relations, functions, injections, surjections, ordinals and
-cardinals. Results proved include Cantor's Theorem, the Recursion
-Theorem, the Schroeder-Bernstein Theorem, and (assuming AC) the
-Wellordering Theorem.
-
-Isabelle/ZF also provides theories of lists, trees, etc., for
-formalizing computational notions. It supports inductive definitions
-of infinite-branching trees for any cardinality of branching.
-
-Useful references for Isabelle/ZF:
-
-
-- Lawrence C. Paulson,
- Set theory for verification: I. From foundations to functions.
- J. Automated Reasoning 11 (1993), 353-389.
-
- - Lawrence C. Paulson,
- Set theory for verification: II. Induction and recursion.
- Report 312, Computer Lab (1993).
-
- - Lawrence C. Paulson,
- A fixedpoint approach to implementing (co)inductive definitions.
- In: A. Bundy (editor),
- CADE-12: 12th International Conference on Automated Deduction,
- (Springer LNAI 814, 1994), 148-161.
-
-
-Useful references on ZF set theory:
-
-
-- Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)
-
-
- Patrick Suppes, Axiomatic Set Theory (Dover, 1972)
-
-
- Keith J. Devlin,
- Fundamentals of Contemporary Set Theory (Springer, 1979)
-
- - Kenneth Kunen
- Set Theory: An Introduction to Independence Proofs
- (North-Holland, 1980)
-
-
-