author | wenzelm |
Sat, 17 Sep 2005 17:35:26 +0200 | |
changeset 17456 | bcf7544875b2 |
parent 1474 | 3f7d67927fe2 |
child 20140 | 98acc6d0fab6 |
permissions | -rw-r--r-- |
(* Title: CCL/ex/Stream.thy ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge *) header {* Programs defined over streams *} theory Stream imports List begin consts iter1 :: "[i=>i,i]=>i" iter2 :: "[i=>i,i]=>i" defs iter1_def: "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)" iter2_def: "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)" ML {* use_legacy_bindings (the_context ()) *} end