isabelle: src/ZF/Coind/ROOT.ML@0140ff702b23 (annotated)

916 d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	1	(* Title: ZF/Coind/MT.ML
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	2	ID: $Id$
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	3	Author: Jacob Frost, Cambridge University Computer Laboratory
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	4	Copyright 1995 University of Cambridge
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	5
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	6	Based upon the article
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	7	Robin Milner and Mads Tofte,
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	8	Co-induction in Relational Semantics,
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	9	Theoretical Computer Science 87 (1991), pages 209-220.
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	10
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	11	Written up as
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	12	Jacob Frost, A Case Study of Co_induction in Isabelle
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	13	Report, Computer Lab, University of Cambridge (1995).
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	14	*)
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	15
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	16	ZF_build_completed; (Make examples fail if ZF did)
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	17
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	18	writeln"Root file for ZF/Coind";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	19	proof_timing := true;
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	20	loadpath := [".","Coind"];
957 28a48c44ca57 Removed exception handlers, as they are now in ZF/Makefile. lcp parents: 916 diff changeset	21	time_use_thy "MT";

author	lcp
	Tue, 25 Apr 1995 11:14:03 +0200
changeset 1072	0140ff702b23
parent 957	28a48c44ca57
child 1296	ae31bb7774a7
permissions	-rw-r--r--