src/HOLCF/ex/dagstuhl.thy
author wenzelm
Sat, 08 Dec 2001 14:41:10 +0100
changeset 12417 e5bdbcec51a3
parent 299 febeb36a4ba4
permissions -rw-r--r--
added General/xml.ML;

(*
    ID:         $ $
*)

Dagstuhl  =  Stream2 +

consts
       YS  :: "'a stream"
       YYS :: "'a stream"

rules

YS_def    "YS  = fix[LAM x. scons[y][x]]"
YYS_def   "YYS = fix[LAM z. scons[y][scons[y][z]]]"
  
end