summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | lcp |

Fri, 14 Apr 1995 12:21:15 +0200 | |

changeset 1062 | c79fb313bf89 |

parent 1061 | 8897213195c0 |

child 1063 | d33e3523a5e6 |

New examples directories Resid and AC

src/ZF/README | file | annotate | diff | comparison | revisions |

--- a/src/ZF/README Fri Apr 14 12:03:15 1995 +0200 +++ b/src/ZF/README Fri Apr 14 12:21:15 1995 +0200 @@ -10,16 +10,25 @@ ROOT.ML -- loads all source files. Enter an ML image containing FOL and type: use "ROOT.ML"; -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"; +There are also several subdirectories of examples. To execute the examples on +some directory <Dir>, enter an ML image containing ZF and type + use "<Dir>/ROOT.ML"; + +AC -- subdirectory containing proofs from the book "Equivalents of the Axiom +of Choice, II" by H. Rubin and J.E. Rubin, 1985. Thanks to Krzysztof +Gr`abczewski. + +Coind -- subdirectory containing a large example of proof by co-induction. It +is by Jacob Frost following a paper by Robin Milner and Mads Tofte. IMP -- subdirectory containing a semantics equivalence proof between operational and denotational definitions of a simple programming language. -To execute, enter an ML image containing ZF and type: use "IMP/ROOT.ML"; +Thanks to Heiko Loetzbeyer & Robert Sandner. -ex -- subdirectory containing examples. To execute them, enter an ML image -containing ZF and type: use "ex/ROOT.ML"; +Resid -- subdirectory containing a proof of the Church-Rosser Theorem. It is +by Ole Rasmussen, following the Coq proof by Gérard Huet. + +ex -- subdirectory containing various examples. Isabelle/ZF formalizes the greater part of elementary set theory, including relations, functions, injections, surjections, ordinals and cardinals.