isabelle: src/ZF/Coind/ROOT.ML@01e83ffa6c54 (annotated)

24584 01e83ffa6c54 fixed title haftmann parents: 12595 diff changeset	1	(* Title: ZF/Coind/ROOT.ML
916 d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1351 diff changeset	3	Author: Jacob Frost, Cambridge University Computer Laboratory
916 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
12595 0480d02221b8 conversion to Isar paulson parents: 9000 diff changeset	16	time_use_thy "ECR";

author	haftmann
	Sat, 15 Sep 2007 19:27:35 +0200
changeset 24584	01e83ffa6c54
parent 12595	0480d02221b8
child 33615	261abc2e3155
permissions	-rw-r--r--