src/HOL/Probability/Discrete_Topology.thy

--- a/src/HOL/Probability/Discrete_Topology.thy	Mon Dec 07 16:48:10 2015 +0000
+++ b/src/HOL/Probability/Discrete_Topology.thy	Mon Dec 07 20:19:59 2015 +0100
@@ -6,7 +6,7 @@
 imports "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
 begin
 
-text {* Copy of discrete types with discrete topology. This space is polish. *}
+text \<open>Copy of discrete types with discrete topology. This space is polish.\<close>
 
 typedef 'a discrete = "UNIV::'a set"
 morphisms of_discrete discrete