changeset 67968 | a5ad4c015d1c |
parent 67613 | ce654b0e6d69 |
child 68527 | 2f4e2aab190a |
--- a/src/HOL/Analysis/Arcwise_Connected.thy Sun Apr 08 12:31:08 2018 +0200 +++ b/src/HOL/Analysis/Arcwise_Connected.thy Mon Apr 09 16:20:23 2018 +0200 @@ -109,7 +109,7 @@ subsection\<open>Arcwise Connections\<close> -subsection\<open>Density of points with dyadic rational coordinates.\<close> +subsection\<open>Density of points with dyadic rational coordinates\<close> proposition closure_dyadic_rationals: "closure (\<Union>k. \<Union>f \<in> Basis \<rightarrow> \<int>.