Now mentions Coind
Wed, 15 Mar 1995 11:25:24 +0100
changeset 958 f2c225386348
parent 957 28a48c44ca57
child 959 35c2e5e114c4
Now mentions Coind
--- 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
+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)