# HG changeset patch
# User huffman
# Date 1126647001 -7200
# Node ID d73f67e90a95c54c5365aa89bf2d8537ee9cc37b
# Parent  923ef4a8c6729447c83a2e7798e7af77e392641f
add theorem chain_const

diff -r 923ef4a8c672 -r d73f67e90a95 src/HOLCF/Porder.ML
--- 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";
diff -r 923ef4a8c672 -r d73f67e90a95 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