src/HOLCF/Sum_Cpo.thy
changeset 35900 aa5dfb03eb1e
parent 31076 99fe356cbbc2
child 37079 0cd15d8c90a0
     1.1 --- a/src/HOLCF/Sum_Cpo.thy	Mon Mar 22 19:29:11 2010 +0100
     1.2 +++ b/src/HOLCF/Sum_Cpo.thy	Mon Mar 22 12:52:51 2010 -0700
     1.3 @@ -8,7 +8,7 @@
     1.4  imports Bifinite
     1.5  begin
     1.6  
     1.7 -subsection {* Ordering on type @{typ "'a + 'b"} *}
     1.8 +subsection {* Ordering on sum type *}
     1.9  
    1.10  instantiation "+" :: (below, below) below
    1.11  begin
    1.12 @@ -128,7 +128,7 @@
    1.13   apply (erule cpo_lubI)
    1.14  done
    1.15  
    1.16 -subsection {* Continuity of @{term Inl}, @{term Inr}, @{term sum_case} *}
    1.17 +subsection {* Continuity of \emph{Inl}, \emph{Inr}, and case function *}
    1.18  
    1.19  lemma cont_Inl: "cont Inl"
    1.20  by (intro contI is_lub_Inl cpo_lubI)