--- a/src/HOLCF/Sprod.thy Mon Mar 22 19:29:11 2010 +0100
+++ b/src/HOLCF/Sprod.thy Mon Mar 22 12:52:51 2010 -0700
@@ -88,7 +88,7 @@
"\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x"
by (cases x, simp_all)
-subsection {* Properties of @{term spair} *}
+subsection {* Properties of \emph{spair} *}
lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>"
by (simp add: Rep_Sprod_simps strictify_conv_if)
@@ -134,7 +134,7 @@
lemma sprodE2: "(\<And>x y. p = (:x, y:) \<Longrightarrow> Q) \<Longrightarrow> Q"
by (cases p, simp only: inst_sprod_pcpo2, simp)
-subsection {* Properties of @{term sfst} and @{term ssnd} *}
+subsection {* Properties of \emph{sfst} and \emph{ssnd} *}
lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_strict)
@@ -208,7 +208,7 @@
apply simp
done
-subsection {* Properties of @{term ssplit} *}
+subsection {* Properties of \emph{ssplit} *}
lemma ssplit1 [simp]: "ssplit\<cdot>f\<cdot>\<bottom> = \<bottom>"
by (simp add: ssplit_def)