| changeset 48722 | a5e3ba7cbb2a |
| parent 48721 | 866f6d5baf4c |
| child 48723 | 0829e958f0aa |
| 48721:866f6d5baf4c | 48722:a5e3ba7cbb2a |
|---|---|
1 (* Title: ZF/Coind/ROOT.ML |
|
2 Author: Jacob Frost, Cambridge University Computer Laboratory |
|
3 Copyright 1995 University of Cambridge |
|
4 |
|
5 Based upon the article |
|
6 Robin Milner and Mads Tofte, |
|
7 Co-induction in Relational Semantics, |
|
8 Theoretical Computer Science 87 (1991), pages 209-220. |
|
9 |
|
10 Written up as |
|
11 Jacob Frost, A Case Study of Co_induction in Isabelle |
|
12 Report, Computer Lab, University of Cambridge (1995). |
|
13 *) |
|
14 |
|
15 use_thys ["ECR"]; |