src/HOL/Lazy_Sequence.thy
changeset 36020 3ee4c29ead7f
parent 34957 3b1957113753
child 36024 c1ce2f60b0f2
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Mon Mar 29 17:30:36 2010 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Mon Mar 29 17:30:38 2010 +0200
     1.3 @@ -131,6 +131,7 @@
     1.4    datatype 'a lazy_sequence = Lazy_Sequence of unit -> ('a * 'a lazy_sequence) option
     1.5    val yield : 'a lazy_sequence -> ('a * 'a lazy_sequence) option
     1.6    val yieldn : int -> 'a lazy_sequence -> ('a list * 'a lazy_sequence)
     1.7 +  val map : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
     1.8  end;
     1.9  
    1.10  structure Lazy_Sequence : LAZY_SEQUENCE =
    1.11 @@ -142,6 +143,8 @@
    1.12  
    1.13  val yieldn = @{code yieldn}
    1.14  
    1.15 +val map = @{code map}
    1.16 +
    1.17  end;
    1.18  *}
    1.19