8 run all the tests described below. |
8 run all the tests described below. |
9 |
9 |
10 ROOT.ML -- loads all source files. Enter an ML image containing FOL and |
10 ROOT.ML -- loads all source files. Enter an ML image containing FOL and |
11 type: use "ROOT.ML"; |
11 type: use "ROOT.ML"; |
12 |
12 |
13 Coind -- subdirectory containing a large example of proof by co-induction, |
13 There are also several subdirectories of examples. To execute the examples on |
14 originally due to Robin Milner and Mads Tofte. To execute, enter an ML image |
14 some directory <Dir>, enter an ML image containing ZF and type |
15 containing ZF and type: use "Coind/ROOT.ML"; |
15 use "<Dir>/ROOT.ML"; |
|
16 |
|
17 AC -- subdirectory containing proofs from the book "Equivalents of the Axiom |
|
18 of Choice, II" by H. Rubin and J.E. Rubin, 1985. Thanks to Krzysztof |
|
19 Gr`abczewski. |
|
20 |
|
21 Coind -- subdirectory containing a large example of proof by co-induction. It |
|
22 is by Jacob Frost following a paper by Robin Milner and Mads Tofte. |
16 |
23 |
17 IMP -- subdirectory containing a semantics equivalence proof between |
24 IMP -- subdirectory containing a semantics equivalence proof between |
18 operational and denotational definitions of a simple programming language. |
25 operational and denotational definitions of a simple programming language. |
19 To execute, enter an ML image containing ZF and type: use "IMP/ROOT.ML"; |
26 Thanks to Heiko Loetzbeyer & Robert Sandner. |
20 |
27 |
21 ex -- subdirectory containing examples. To execute them, enter an ML image |
28 Resid -- subdirectory containing a proof of the Church-Rosser Theorem. It is |
22 containing ZF and type: use "ex/ROOT.ML"; |
29 by Ole Rasmussen, following the Coq proof by Gérard Huet. |
|
30 |
|
31 ex -- subdirectory containing various examples. |
23 |
32 |
24 Isabelle/ZF formalizes the greater part of elementary set theory, including |
33 Isabelle/ZF formalizes the greater part of elementary set theory, including |
25 relations, functions, injections, surjections, ordinals and cardinals. |
34 relations, functions, injections, surjections, ordinals and cardinals. |
26 Results proved include Cantor's Theorem, the Recursion Theorem, the |
35 Results proved include Cantor's Theorem, the Recursion Theorem, the |
27 Schroeder-Bernstein Theorem, and (assuming AC) the Wellordering Theorem. |
36 Schroeder-Bernstein Theorem, and (assuming AC) the Wellordering Theorem. |