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

1474 3f7d67927fe2 expanded tabs clasohm parents: 290 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	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	paulson
	Wed, 05 Jul 2000 17:42:06 +0200
changeset 9249	c71db8c28727
parent 1474	3f7d67927fe2
child 17456	bcf7544875b2
permissions	-rw-r--r--