src/HOLCF/Product_Cpo.thy
changeset 35900 aa5dfb03eb1e
parent 33506 afb577487b15
child 35914 91a7311177c4
     1.1 --- a/src/HOLCF/Product_Cpo.thy	Mon Mar 22 19:29:11 2010 +0100
     1.2 +++ b/src/HOLCF/Product_Cpo.thy	Mon Mar 22 12:52:51 2010 -0700
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  defaultsort cpo
     1.6  
     1.7 -subsection {* Type @{typ unit} is a pcpo *}
     1.8 +subsection {* Unit type is a pcpo *}
     1.9  
    1.10  instantiation unit :: below
    1.11  begin
    1.12 @@ -58,7 +58,7 @@
    1.13      by (fast intro: below_trans)
    1.14  qed
    1.15  
    1.16 -subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
    1.17 +subsection {* Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd} *}
    1.18  
    1.19  lemma prod_belowI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
    1.20  unfolding below_prod_def by simp
    1.21 @@ -187,7 +187,7 @@
    1.22  lemma split_strict [simp]: "split f \<bottom> = f \<bottom> \<bottom>"
    1.23  unfolding split_def by simp
    1.24  
    1.25 -subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
    1.26 +subsection {* Continuity of \emph{Pair}, \emph{fst}, \emph{snd} *}
    1.27  
    1.28  lemma cont_pair1: "cont (\<lambda>x. (x, y))"
    1.29  apply (rule contI)