Up to index of Isabelle/HOLCF/ex
theory Dagstuhl(* $Id: Dagstuhl.thy,v 1.7 2005/09/06 17:28:58 wenzelm Exp $ *) 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