src/HOLCF/Porder.thy

 apply (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI)
 done
 
 text {* the lub of a constant chain is the constant *}
 
+lemma chain_const: "chain (\<lambda>i. c)"
+by (simp add: chainI)
+
 lemma lub_const: "range(%x. c) <<| c"
 apply (blast dest: ub_rangeD intro: is_lubI ub_rangeI)
 done
 
 lemmas thelub_const = lub_const [THEN thelubI, standard]