--- a/src/CCL/ex/Stream.thy Sat Sep 17 14:02:31 2005 +0200
+++ b/src/CCL/ex/Stream.thy Sat Sep 17 17:35:26 2005 +0200
@@ -1,20 +1,24 @@
-(* Title: CCL/ex/stream.thy
+(* Title: CCL/ex/Stream.thy
ID: $Id$
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-
-Programs defined over streams.
*)
-Stream = List +
+header {* Programs defined over streams *}
+
+theory Stream
+imports List
+begin
consts
+ iter1 :: "[i=>i,i]=>i"
+ iter2 :: "[i=>i,i]=>i"
- iter1,iter2 :: "[i=>i,i]=>i"
+defs
-rules
+ 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)"
- 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