author | paulson |
Fri, 18 Feb 2000 15:35:29 +0100 | |
changeset 8255 | 38f96394c099 |
parent 6349 | f7750d816c21 |
child 9000 | c20d58286a51 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/Coind/MT.ML |
916 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Jacob Frost, Cambridge University Computer Laboratory |
916 | 4 |
Copyright 1995 University of Cambridge |
5 |
||
6 |
Based upon the article |
|
7 |
Robin Milner and Mads Tofte, |
|
8 |
Co-induction in Relational Semantics, |
|
9 |
Theoretical Computer Science 87 (1991), pages 209-220. |
|
10 |
||
11 |
Written up as |
|
12 |
Jacob Frost, A Case Study of Co_induction in Isabelle |
|
13 |
Report, Computer Lab, University of Cambridge (1995). |
|
14 |
*) |
|
15 |
||
6349
f7750d816c21
removed foo_build_completed -- now handled by session management (via usedir);
wenzelm
parents:
4446
diff
changeset
|
16 |
writeln"Root file for ZF/Coind"; |
916 | 17 |
|
4446 | 18 |
set proof_timing; |
957
28a48c44ca57
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
916
diff
changeset
|
19 |
time_use_thy "MT"; |