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

0 a5a9c433f639 Initial revision clasohm parents: diff changeset	1	(* Title: CCL/ex/stream.thy
a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
a5a9c433f639 Initial revision clasohm parents: diff changeset	3	Author: Martin Coen, Cambridge University Computer Laboratory
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	Programs defined over streams.
a5a9c433f639 Initial revision clasohm parents: diff changeset	7	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	8
a5a9c433f639 Initial revision clasohm parents: diff changeset	9	Stream = List +
a5a9c433f639 Initial revision clasohm parents: diff changeset	10
a5a9c433f639 Initial revision clasohm parents: diff changeset	11	consts
a5a9c433f639 Initial revision clasohm parents: diff changeset	12
a5a9c433f639 Initial revision clasohm parents: diff changeset	13	iter1,iter2 :: "[i=>i,i]=>i"
a5a9c433f639 Initial revision clasohm parents: diff changeset	14
a5a9c433f639 Initial revision clasohm parents: diff changeset	15	rules
a5a9c433f639 Initial revision clasohm parents: diff changeset	16
a5a9c433f639 Initial revision clasohm parents: diff changeset	17	iter1_def "iter1(f,a) == letrec iter x be x.iter(f(x)) in iter(a)"
a5a9c433f639 Initial revision clasohm parents: diff changeset	18	iter2_def "iter2(f,a) == letrec iter x be x.map(f,iter(x)) in iter(a)"
a5a9c433f639 Initial revision clasohm parents: diff changeset	19
a5a9c433f639 Initial revision clasohm parents: diff changeset	20	end

author	clasohm
	Thu, 16 Sep 1993 12:20:38 +0200
changeset 0	a5a9c433f639
child 290	37d580c16af5
permissions	-rw-r--r--