changeset 40327 | 1dfdbd66093a |
parent 40322 | 707eb30e8a53 |
child 40329 | 73f2b99b549d |
--- a/src/HOLCF/Library/Stream.thy Fri Oct 29 16:51:40 2010 -0700 +++ b/src/HOLCF/Library/Stream.thy Fri Oct 29 17:15:28 2010 -0700 @@ -921,7 +921,7 @@ by (rule monofun_cfun_arg,simp) lemma contlub_scons_lemma: "chain S ==> (LUB i. a && S i) = a && (LUB i. S i)" -by (rule cont2contlubE [OF cont_Rep_CFun2, symmetric]) +by (rule cont2contlubE [OF cont_Rep_cfun2, symmetric]) lemma finite_lub_sconc: "chain Y ==> (stream_finite x) ==> (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"