New examples directories Resid and AC
authorlcp
Fri Apr 14 12:21:15 1995 +0200 (1995-04-14)
changeset 1062c79fb313bf89
parent 1061 8897213195c0
child 1063 d33e3523a5e6
New examples directories Resid and AC
src/ZF/README
     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.