# HG changeset patch
# User huffman
# Date 1286990846 25200
# Node ID d7fdd84b959f8f685d52b5c789b8832ed76dc6f7
# Parent  f2c78550c0b7ac1b1aab32e712b83df36445050e
edit comments

diff -r f2c78550c0b7 -r d7fdd84b959f src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Tue Oct 12 09:32:21 2010 -0700
+++ b/src/HOLCF/Cont.thy	Wed Oct 13 10:27:26 2010 -0700
@@ -189,7 +189,7 @@
 
 subsection {* Finite chains and flat pcpos *}
 
-text {* monotone functions map finite chains to finite chains *}
+text {* Monotone functions map finite chains to finite chains. *}
 
 lemma monofun_finch2finch:
   "\<lbrakk>monofun f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))"
@@ -198,12 +198,14 @@
 apply (force simp add: max_in_chain_def)
 done
 
-text {* The same holds for continuous functions *}
+text {* The same holds for continuous functions. *}
 
 lemma cont_finch2finch:
   "\<lbrakk>cont f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))"
 by (rule cont2mono [THEN monofun_finch2finch])
 
+text {* All monotone functions with chain-finite domain are continuous. *}
+
 lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont (f::'a::chfin \<Rightarrow> 'b::cpo)"
 apply (erule contI2)
 apply (frule chfin2finch)
@@ -213,7 +215,7 @@
 apply (force simp add: max_in_chain_def)
 done
 
-text {* some properties of flat *}
+text {* All strict functions with flat domain are continuous. *}
 
 lemma flatdom_strict2mono: "f \<bottom> = \<bottom> \<Longrightarrow> monofun (f::'a::flat \<Rightarrow> 'b::pcpo)"
 apply (rule monofunI)
@@ -224,7 +226,7 @@
 lemma flatdom_strict2cont: "f \<bottom> = \<bottom> \<Longrightarrow> cont (f::'a::flat \<Rightarrow> 'b::pcpo)"
 by (rule flatdom_strict2mono [THEN chfindom_monofun2cont])
 
-text {* functions with discrete domain *}
+text {* All functions with discrete domain are continuous. *}
 
 lemma cont_discrete_cpo [simp, cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
 apply (rule contI)