# HG changeset patch
# User lcp
# Date 795263124 -3600
# Node ID f2c225386348557020b7f754762e7b68f40444ef
# Parent  28a48c44ca571e2de9e13c88313fcbe6a4385c2f
Now mentions Coind

diff -r 28a48c44ca57 -r f2c225386348 src/ZF/README
--- 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$