src/HOLCF/ex/Dagstuhl.thy

converted to Isar theory format;

(* $Id$ *)

theory Dagstuhl
imports Stream
begin

consts
  y  :: "'a"

constdefs
  YS :: "'a stream"
  "YS == fix$(LAM x. y && x)"
  YYS :: "'a stream"
  "YYS == fix$(LAM z. y && y && z)"

ML {* use_legacy_bindings (the_context ()) *}

end