diff -r ce36bed06dee -r b5163b2132c5 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Tue Jan 22 21:16:48 2019 +0000
+++ b/src/HOL/Analysis/Function_Topology.thy	Tue Jan 22 22:57:16 2019 +0000
@@ -7,7 +7,7 @@
 begin
 
 
-section%important \<open>Product Topology\<close>
+section \<open>Product Topology\<close> (* FIX  see comments by the author *)
 
 text \<open>We want to define the product topology.
 
@@ -63,7 +63,7 @@
 
 subsection \<open>Topology without type classes\<close>
 
-subsubsection \<open>The topology generated by some (open) subsets\<close>
+subsubsection%important \<open>The topology generated by some (open) subsets\<close>
 
 text \<open>In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
 as it follows from \<open>UN\<close> taking for \<open>K\<close> the empty set. However, it is convenient to have,
@@ -257,7 +257,7 @@
   qed
 qed
 
-subsubsection \<open>Continuity\<close>
+subsubsection%important \<open>Continuity\<close>
 
 text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
 of type classes, as defined below.\<close>
@@ -335,7 +335,7 @@
 using assms unfolding continuous_on_topo_def by auto
 
 
-subsubsection \<open>Pullback topology\<close>
+subsubsection%important \<open>Pullback topology\<close>
 
 text \<open>Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
 a special case of this notion, pulling back by the identity. We introduce the general notion as
@@ -808,7 +808,7 @@
 qed
 
 
-subsubsection \<open>Powers of a single topological space as a topological space, using type classes\<close>
+subsubsection%important \<open>Powers of a single topological space as a topological space, using type classes\<close>
 
 instantiation "fun" :: (type, topological_space) topological_space
 begin
@@ -884,7 +884,7 @@
   "continuous_on UNIV f \<longleftrightarrow> (\<forall>i. continuous_on UNIV (\<lambda>x. f x i))"
 by (auto intro: continuous_on_product_then_coordinatewise)
 
-subsubsection \<open>Topological countability for product spaces\<close>
+subsubsection%important \<open>Topological countability for product spaces\<close>
 
 text \<open>The next two lemmas are useful to prove first or second countability
 of product spaces, but they have more to do with countability and could