--- a/src/ZF/README Wed Mar 15 11:01:08 1995 +0100
+++ b/src/ZF/README Wed Mar 15 11:25:24 1995 +0100
@@ -4,10 +4,15 @@
ZF Set Theory. It is loaded upon FOL, not Pure Isabelle. Important files
include
+Makefile -- compiles the files under Poly/ML or SML of New Jersey. Can also
+run all the tests described below.
+
ROOT.ML -- loads all source files. Enter an ML image containing FOL and
type: use "ROOT.ML";
-Makefile -- compiles the files under Poly/ML or SML of New Jersey
+Coind -- subdirectory containing a large example of proof by co-induction,
+originally due to Robin Milner and Mads Tofte. To execute, enter an ML image
+containing ZF and type: use "Coind/ROOT.ML";
IMP -- subdirectory containing a semantics equivalence proof between
operational and denotational definitions of a simple programming language.
@@ -53,3 +58,5 @@
Kenneth Kunen
Set Theory: An Introduction to Independence Proofs
(North-Holland, 1980)
+
+$Id$