equal
deleted
inserted
replaced
1 <!-- $Id$ --> |
1 <!-- $Id$ --> |
2 <HTML><HEAD><TITLE>ZF/Coind</TITLE></HEAD><BODY> |
2 <HTML><HEAD><TITLE>ZF/Coind/README</TITLE></HEAD><BODY> |
3 |
3 |
4 <H2>Coind -- A Coinduction Example</H2> |
4 <H2>Coind -- A Coinduction Example</H2> |
5 |
5 |
6 Jacob Frost has mechanized the proofs from the article |
6 Jacob Frost has mechanized the proofs from the article |
7 |
7 |
24 |
24 |
25 <P> |
25 <P> |
26 Frost's |
26 Frost's |
27 <A |
27 <A |
28 HREF="http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz">report</A> describes this development. |
28 HREF="http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz">report</A> describes this development. |
29 <P> |
|
30 |
29 |
31 <HR> |
30 </body> |
32 |
31 </html> |
33 <P>Last modified 5 March 1996 |
|
34 |
|
35 <ADDRESS> |
|
36 <P><A HREF="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C. Paulson</A> / |
|
37 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A> |
|
38 </ADDRESS> |
|