--- a/src/HOL/Lazy_Sequence.thy Mon Mar 29 17:30:36 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy Mon Mar 29 17:30:38 2010 +0200
@@ -131,6 +131,7 @@
datatype 'a lazy_sequence = Lazy_Sequence of unit -> ('a * 'a lazy_sequence) option
val yield : 'a lazy_sequence -> ('a * 'a lazy_sequence) option
val yieldn : int -> 'a lazy_sequence -> ('a list * 'a lazy_sequence)
+ val map : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
end;
structure Lazy_Sequence : LAZY_SEQUENCE =
@@ -142,6 +143,8 @@
val yieldn = @{code yieldn}
+val map = @{code map}
+
end;
*}