--- a/src/HOLCF/Sum_Cpo.thy Mon Mar 22 19:29:11 2010 +0100
+++ b/src/HOLCF/Sum_Cpo.thy Mon Mar 22 12:52:51 2010 -0700
@@ -8,7 +8,7 @@
imports Bifinite
begin
-subsection {* Ordering on type @{typ "'a + 'b"} *}
+subsection {* Ordering on sum type *}
instantiation "+" :: (below, below) below
begin
@@ -128,7 +128,7 @@
apply (erule cpo_lubI)
done
-subsection {* Continuity of @{term Inl}, @{term Inr}, @{term sum_case} *}
+subsection {* Continuity of \emph{Inl}, \emph{Inr}, and case function *}
lemma cont_Inl: "cont Inl"
by (intro contI is_lub_Inl cpo_lubI)