isabelle: src/CCL/ex/Stream.thy@bcf7544875b2 (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	wenzelm
	Sat, 17 Sep 2005 17:35:26 +0200
changeset 17456	bcf7544875b2
parent 1474	3f7d67927fe2
child 20140	98acc6d0fab6
permissions	-rw-r--r--