src/HOLCF/Porder.thy

--- a/src/HOLCF/Porder.thy	Tue Sep 13 22:49:12 2005 +0200
+++ b/src/HOLCF/Porder.thy	Tue Sep 13 23:30:01 2005 +0200
@@ -265,6 +265,9 @@
 
 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