src/HOLCF/ex/dagstuhl.thy
changeset 13897 f62f9a75f685
parent 13896 717bd79b976f
child 13898 9410d2eb9563
equal deleted inserted replaced
13896:717bd79b976f 13897:f62f9a75f685
     1 (*
       
     2     ID:         $ $
       
     3 *)
       
     4 
       
     5 Dagstuhl  =  Stream2 +
       
     6 
       
     7 consts
       
     8        YS  :: "'a stream"
       
     9        YYS :: "'a stream"
       
    10 
       
    11 rules
       
    12 
       
    13 YS_def    "YS  = fix[LAM x. scons[y][x]]"
       
    14 YYS_def   "YYS = fix[LAM z. scons[y][scons[y][z]]]"
       
    15   
       
    16 end
       
    17