Put in minimal simpset to avoid excessive simplification,
just as in revision 1.9 of HOL/indrule.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