src/HOLCF/ex/Stream.thy
changeset 14535 7cb26928e70d
parent 14171 0cab06e3bbd0
child 14981 e73f8140af78
equal deleted inserted replaced
14534:7a46bdcd92f2 14535:7cb26928e70d
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author: 	Franz Regensburger, David von Oheimb
     3     Author: 	Franz Regensburger, David von Oheimb
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     5 
     6 General Stream domain.
     6 General Stream domain.
       
     7 TODO: should be integrated with HOLCF/Streams
     7 *)
     8 *)
     8 
     9 
     9 Stream = HOLCF + Nat_Infinity +
    10 Stream = HOLCF + Nat_Infinity +
    10 
    11 
    11 domain 'a stream = "&&" (ft::'a) (lazy rt::'a stream) (infixr 65)
    12 domain 'a stream = "&&" (ft::'a) (lazy rt::'a stream) (infixr 65)