diff -r 92e0028a46f2 -r 5d200f2d7a4f src/HOLCF/Pcpo.thy --- a/src/HOLCF/Pcpo.thy Mon Mar 01 17:32:23 2010 -0800 +++ b/src/HOLCF/Pcpo.thy Mon Mar 01 19:18:08 2010 -0800 @@ -91,6 +91,10 @@ \ (\i. X i) = (\i. Y i)" by (simp only: expand_fun_eq [symmetric]) +lemma lub_eq: + "(\i. X i = Y i) \ (\i. X i) = (\i. Y i)" + by simp + text {* more results about mono and = of lubs of chains *} lemma lub_mono2: