author | clasohm |
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06) | |
changeset 1478 | 2b8c2a7547ab |
parent 1461 | 6bcb44e4d6e5 |
child 4446 | 097004a470fb |
permissions | -rw-r--r-- |
clasohm@1461 | 1 |
(* Title: ZF/Coind/MT.ML |
lcp@916 | 2 |
ID: $Id$ |
clasohm@1461 | 3 |
Author: Jacob Frost, Cambridge University Computer Laboratory |
lcp@916 | 4 |
Copyright 1995 University of Cambridge |
lcp@916 | 5 |
|
lcp@916 | 6 |
Based upon the article |
lcp@916 | 7 |
Robin Milner and Mads Tofte, |
lcp@916 | 8 |
Co-induction in Relational Semantics, |
lcp@916 | 9 |
Theoretical Computer Science 87 (1991), pages 209-220. |
lcp@916 | 10 |
|
lcp@916 | 11 |
Written up as |
lcp@916 | 12 |
Jacob Frost, A Case Study of Co_induction in Isabelle |
lcp@916 | 13 |
Report, Computer Lab, University of Cambridge (1995). |
lcp@916 | 14 |
*) |
lcp@916 | 15 |
|
clasohm@1461 | 16 |
ZF_build_completed; (*Make examples fail if ZF did*) |
lcp@916 | 17 |
|
lcp@916 | 18 |
writeln"Root file for ZF/Coind"; |
lcp@916 | 19 |
proof_timing := true; |
clasohm@1351 | 20 |
|
lcp@957 | 21 |
time_use_thy "MT"; |