export somehow odd mapa explicitly
authorhaftmann
Wed Apr 28 17:04:56 2010 +0200 (2010-04-28)
changeset 365168dac276ab10d
parent 36515 4073bf588746
child 36517 0dcd03d521ec
child 36526 353041483b9b
export somehow odd mapa explicitly
src/HOL/Lazy_Sequence.thy
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Wed Apr 28 16:56:19 2010 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Wed Apr 28 17:04:56 2010 +0200
     1.3 @@ -125,10 +125,10 @@
     1.4  
     1.5  code_reflect
     1.6    datatypes lazy_sequence = Lazy_Sequence
     1.7 -  functions "Lazy_Sequence.map" yield
     1.8 +  functions map yield
     1.9    module_name Lazy_Sequence
    1.10  
    1.11 -(* FIXME formulate yieldn in the logic with type code_numeral *)
    1.12 +(* FIXME formulate yieldn in the logic with type code_numeral -- get rid of mapa confusion *)
    1.13  
    1.14  ML {*
    1.15  signature LAZY_SEQUENCE =
    1.16 @@ -137,6 +137,7 @@
    1.17    val yield : 'a lazy_sequence -> ('a * 'a lazy_sequence) option
    1.18    val yieldn : int -> 'a lazy_sequence -> ('a list * 'a lazy_sequence)
    1.19    val map : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
    1.20 +  val mapa : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
    1.21  end;
    1.22  
    1.23  structure Lazy_Sequence : LAZY_SEQUENCE =