1.1 --- a/src/ZF/README Fri Apr 14 12:03:15 1995 +0200
1.2 +++ b/src/ZF/README Fri Apr 14 12:21:15 1995 +0200
1.3 @@ -10,16 +10,25 @@
1.4 ROOT.ML -- loads all source files. Enter an ML image containing FOL and
1.5 type: use "ROOT.ML";
1.6
1.7 -Coind -- subdirectory containing a large example of proof by co-induction,
1.8 -originally due to Robin Milner and Mads Tofte. To execute, enter an ML image
1.9 -containing ZF and type: use "Coind/ROOT.ML";
1.10 +There are also several subdirectories of examples. To execute the examples on
1.11 +some directory <Dir>, enter an ML image containing ZF and type
1.12 + use "<Dir>/ROOT.ML";
1.13 +
1.14 +AC -- subdirectory containing proofs from the book "Equivalents of the Axiom
1.15 +of Choice, II" by H. Rubin and J.E. Rubin, 1985. Thanks to Krzysztof
1.16 +Gr`abczewski.
1.17 +
1.18 +Coind -- subdirectory containing a large example of proof by co-induction. It
1.19 +is by Jacob Frost following a paper by Robin Milner and Mads Tofte.
1.20
1.21 IMP -- subdirectory containing a semantics equivalence proof between
1.22 operational and denotational definitions of a simple programming language.
1.23 -To execute, enter an ML image containing ZF and type: use "IMP/ROOT.ML";
1.24 +Thanks to Heiko Loetzbeyer & Robert Sandner.
1.25
1.26 -ex -- subdirectory containing examples. To execute them, enter an ML image
1.27 -containing ZF and type: use "ex/ROOT.ML";
1.28 +Resid -- subdirectory containing a proof of the Church-Rosser Theorem. It is
1.29 +by Ole Rasmussen, following the Coq proof by Gérard Huet.
1.30 +
1.31 +ex -- subdirectory containing various examples.
1.32
1.33 Isabelle/ZF formalizes the greater part of elementary set theory, including
1.34 relations, functions, injections, surjections, ordinals and cardinals.