equal
deleted
inserted
replaced
|
1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
|
2 |
1 <HTML><HEAD><TITLE>ZF/README</TITLE></HEAD><BODY> |
3 <HTML><HEAD><TITLE>ZF/README</TITLE></HEAD><BODY> |
2 |
4 |
3 <H2>ZF: Zermelo-Fraenkel Set Theory</H2> |
5 <H2>ZF: Zermelo-Fraenkel Set Theory</H2> |
4 |
6 |
5 This directory contains the ML sources of the Isabelle system for |
7 This directory contains the ML sources of the Isabelle system for |
21 operational and denotational definitions of a simple programming language. |
23 operational and denotational definitions of a simple programming language. |
22 Thanks to Heiko Loetzbeyer & Robert Sandner.<P> |
24 Thanks to Heiko Loetzbeyer & Robert Sandner.<P> |
23 |
25 |
24 <DT>Resid |
26 <DT>Resid |
25 <DD>subdirectory containing a proof of the Church-Rosser Theorem. It is |
27 <DD>subdirectory containing a proof of the Church-Rosser Theorem. It is |
26 by Ole Rasmussen, following the Coq proof by Gérard Huet.<P> |
28 by Ole Rasmussen, following the Coq proof by G�ard Huet.<P> |
27 |
29 |
28 <DT>ex |
30 <DT>ex |
29 <DD>subdirectory containing various examples. |
31 <DD>subdirectory containing various examples. |
30 </DL> |
32 </DL> |
31 |
33 |