isabelle: src/CCL/ex/Stream.thy@b3e7da94b51f (annotated)

17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	1	(* Title: CCL/ex/Stream.thy
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
1474 3f7d67927fe2 expanded tabs clasohm parents: 290 diff changeset	3	Author: Martin Coen, Cambridge University Computer Laboratory
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1993 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	6
17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	7	header {* Programs defined over streams *}
bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	8
bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	9	theory Stream
bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	10	imports List
bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	11	begin
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	12
a5a9c433f639 Initial revision clasohm parents: diff changeset	13	consts
17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	14	iter1 :: "[i=>i,i]=>i"
bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	15	iter2 :: "[i=>i,i]=>i"
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	16
17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	17	defs
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	18
17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	19	iter1_def: "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)"
bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	20	iter2_def: "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)"
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	21
17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	22	ML {* use_legacy_bindings (the_context ()) *}
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	23
a5a9c433f639 Initial revision clasohm parents: diff changeset	24	end

author	urbanc
	Tue, 13 Dec 2005 18:11:21 +0100
changeset 18396	b3e7da94b51f
parent 17456	bcf7544875b2
child 20140	98acc6d0fab6
permissions	-rw-r--r--