--- a/src/HOL/HOLCF/Discrete.thy Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Discrete.thy Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
Author: Tobias Nipkow
*)
-section {* Discrete cpo types *}
+section \<open>Discrete cpo types\<close>
theory Discrete
imports Cont
@@ -10,7 +10,7 @@
datatype 'a discr = Discr "'a :: type"
-subsection {* Discrete cpo class instance *}
+subsection \<open>Discrete cpo class instance\<close>
instantiation discr :: (type) discrete_cpo
begin
@@ -23,7 +23,7 @@
end
-subsection {* \emph{undiscr} *}
+subsection \<open>\emph{undiscr}\<close>
definition
undiscr :: "('a::type)discr => 'a" where