src/HOLCF/Universal.thy

 apply (rule finite_subset [where B="insert 0 {x. P x}"])
 apply (clarsimp simp add: ubasis_until')
 apply simp
 done
 
-subsubsection {* Take function for @{typ ubasis} *}
+subsubsection {* Take function for \emph{ubasis} *}
 
 definition
   ubasis_take :: "nat \<Rightarrow> ubasis \<Rightarrow> ubasis"
 where
   "ubasis_take n = ubasis_until (\<lambda>x. x \<le> n)"

   "\<exists>a\<in>Rep_udom x. approx n\<cdot>x = udom_principal (ubasis_take n a)"
 unfolding approx_udom_def
 by (rule udom.completion_approx_eq_principal)
 
 
-subsection {* Universality of @{typ udom} *}
+subsection {* Universality of \emph{udom} *}
 
 defaultsort bifinite
 
 subsubsection {* Choosing a maximal element from a finite set *}
 

   choose
   choose_pos
   place
   sub
 
-subsubsection {* EP-pair from any bifinite domain into @{typ udom} *}
+subsubsection {* EP-pair from any bifinite domain into \emph{udom} *}
 
 definition
   udom_emb :: "'a::bifinite \<rightarrow> udom"
 where
   "udom_emb = compact_basis.basis_fun (\<lambda>x. udom_principal (basis_emb x))"