isabelle: src/ZF/Coind/ROOT.ML@217ca1273786 (annotated)

24584 01e83ffa6c54 fixed title haftmann parents: 12595 diff changeset	1	(* Title: ZF/Coind/ROOT.ML
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1351 diff changeset	2	Author: Jacob Frost, Cambridge University Computer Laboratory
916 d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	3	Copyright 1995 University of Cambridge
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	4
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	5	Based upon the article
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	6	Robin Milner and Mads Tofte,
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	7	Co-induction in Relational Semantics,
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	8	Theoretical Computer Science 87 (1991), pages 209-220.
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	9
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	10	Written up as
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	11	Jacob Frost, A Case Study of Co_induction in Isabelle
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	12	Report, Computer Lab, University of Cambridge (1995).
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	13	*)
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	14
33615 261abc2e3155 uniform use of simultabeous use_thys; wenzelm parents: 24584 diff changeset	15	use_thys ["ECR"];

author	blanchet
	Mon, 19 Apr 2010 15:15:21 +0200
changeset 36223	217ca1273786
parent 33615	261abc2e3155
permissions	-rw-r--r--