src/ZF/README.html
changeset 51403 2ff3a5589b05
parent 51402 b05cd411d3d3
child 51404 90a598019aeb
--- 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 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<HTML>
-
-<HEAD>
-  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
-  <TITLE>ZF/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>ZF: Zermelo-Fraenkel Set Theory</H2>
-
-This directory contains the ML sources of the Isabelle system for
-ZF Set Theory, based on FOL.<p>
-
-There are several subdirectories of examples:
-<DL>
-<DT>AC
-<DD>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.<P>
-
-<DT>Coind
-<DD>subdirectory containing a large example of proof by co-induction.  It
-is by Jacob Frost following a paper by Robin Milner and Mads Tofte.<P>
-
-<DT>IMP
-<DD>subdirectory containing a semantics equivalence proof between
-operational and denotational definitions of a simple programming language.
-Thanks to Heiko Loetzbeyer & Robert Sandner.<P>
-
-<DT>Resid
-<DD>subdirectory containing a proof of the Church-Rosser Theorem.  It is
-by Ole Rasmussen, following the Coq proof by G�ard Huet.<P>
-
-<DT>ex
-<DD>subdirectory containing various examples.
-</DL>
-
-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.<P>
-
-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.<P>
-
-Useful references for Isabelle/ZF:
-
-<UL>
-<LI>	Lawrence C. Paulson,<BR>
-	Set theory for verification: I. From foundations to functions.<BR>
-	J. Automated Reasoning 11 (1993), 353-389.
-
-<LI>	Lawrence C. Paulson,<BR>
-	Set theory for verification: II. Induction and recursion.<BR>
-	Report 312, Computer Lab (1993).<BR>
-
-<LI>	Lawrence C. Paulson,<BR>
-	A fixedpoint approach to implementing (co)inductive definitions. <BR> 
-	In: A. Bundy (editor),<BR>
-	CADE-12: 12th International Conference on Automated Deduction,<BR>
-	(Springer LNAI 814, 1994), 148-161.
-</UL>
-
-Useful references on ZF set theory:
-
-<UL>
-<LI>	Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)
-
-<LI>	Patrick Suppes, Axiomatic Set Theory (Dover, 1972)
-
-<LI>	Keith J. Devlin,<BR>
-	Fundamentals of Contemporary Set Theory (Springer, 1979)
-
-<LI>	Kenneth Kunen<BR>
-	Set Theory: An Introduction to Independence Proofs<BR>
-	(North-Holland, 1980)
-</UL>
-
-</BODY></HTML>