add lemma cpo_lubI

--- a/src/HOLCF/Pcpo.thy	Thu Jan 31 21:23:14 2008 +0100
+++ b/src/HOLCF/Pcpo.thy	Thu Jan 31 21:37:20 2008 +0100
@@ -19,6 +19,9 @@
 
 text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
 
+lemma cpo_lubI: "chain (S::nat \<Rightarrow> 'a::cpo) \<Longrightarrow> range S <<| lub (range S)"
+by (fast dest: cpo elim: lubI)
+
 lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = (l::'a::cpo)\<rbrakk> \<Longrightarrow> range S <<| l"
 by (blast dest: cpo intro: lubI)