isabelle: src/CCL/ex/stream.thy@b9fc536792bb (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
290 37d580c16af5 changed "." to "$" and added parentheses to eliminate ambiguity clasohm parents: 0 diff changeset	17	iter1_def "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)"
37d580c16af5 changed "." to "$" and added parentheses to eliminate ambiguity clasohm parents: 0 diff changeset	18	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	19
a5a9c433f639 Initial revision clasohm parents: diff changeset	20	end

author	lcp
	Thu, 03 Nov 1994 12:39:39 +0100
changeset 691	b9fc536792bb
parent 290	37d580c16af5
permissions	-rw-r--r--