src/HOLCF/explicit_domains/Dagstuhl.thy

removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2

(* $Id$ *)


Dagstuhl  =  Stream2 +

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

defs

YS_def    "YS  == fix`(LAM x. scons`y`x)"
YYS_def   "YYS == fix`(LAM z. scons`y`(scons`y`z))"
  
end