add theorem chain_const

--- a/src/HOLCF/Porder.ML	Tue Sep 13 22:49:12 2005 +0200
+++ b/src/HOLCF/Porder.ML	Tue Sep 13 23:30:01 2005 +0200
@@ -9,6 +9,7 @@
 val chain_def = thm "chain_def";
 val chainE = thm "chainE";
 val chainI = thm "chainI";
+val chain_const = thm "chain_const";
 val chain_mono3 = thm "chain_mono3";
 val chain_mono = thm "chain_mono";
 val chain_shift = thm "chain_shift";

--- 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