changeset 61808 | fc1556774cfe |
parent 51343 | b61b32f62c78 |
child 62101 | 26c0a70f78a3 |
--- 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