src/HOL/HOLCF/Discrete.thy

 (*  Title:      HOL/HOLCF/Discrete.thy
     Author:     Tobias Nipkow
 *)
 
-section {* Discrete cpo types *}
+section \<open>Discrete cpo types\<close>
 
 theory Discrete
 imports Cont
 begin
 
 datatype 'a discr = Discr "'a :: type"
 
-subsection {* Discrete cpo class instance *}
+subsection \<open>Discrete cpo class instance\<close>
 
 instantiation discr :: (type) discrete_cpo
 begin
 
 definition

 instance
   by standard (simp add: below_discr_def)
 
 end
 
-subsection {* \emph{undiscr} *}
+subsection \<open>\emph{undiscr}\<close>
 
 definition
   undiscr :: "('a::type)discr => 'a" where
   "undiscr x = (case x of Discr y => y)"