diff -r 500a7acdccd4 -r 8b3458ca0762 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Function_Topology.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -61,9 +61,9 @@
 I realized afterwards that this theory has a lot in common with \<^file>\<open>~~/src/HOL/Library/Finite_Map.thy\<close>.
 \<close>
 
-subsection%important \<open>Topology without type classes\<close>
+subsection \<open>Topology without type classes\<close>
 
-subsubsection%important \<open>The topology generated by some (open) subsets\<close>
+subsubsection \<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%important \<open>Continuity\<close>
+subsubsection \<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>
@@ -336,7 +336,7 @@
 using assms unfolding continuous_on_topo_def by auto
 
 
-subsubsection%important \<open>Pullback topology\<close>
+subsubsection \<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
@@ -425,7 +425,7 @@
 qed
 
 
-subsection%important \<open>The product topology\<close>
+subsection \<open>The product topology\<close>
 
 text \<open>We can now define the product topology, as generated by
 the sets which are products of open sets along finitely many coordinates, and the whole
@@ -809,7 +809,7 @@
 qed
 
 
-subsubsection%important \<open>Powers of a single topological space as a topological space, using type classes\<close>
+subsubsection \<open>Powers of a single topological space as a topological space, using type classes\<close>
 
 instantiation "fun" :: (type, topological_space) topological_space
 begin
@@ -885,7 +885,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%important \<open>Topological countability for product spaces\<close>
+subsubsection \<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
@@ -1116,7 +1116,7 @@
   using product_topology_countable_basis topological_basis_imp_subbasis by auto
 
 
-subsection%important \<open>The strong operator topology on continuous linear operators\<close> (* FIX ME mv*)
+subsection \<open>The strong operator topology on continuous linear operators\<close> (* FIX ME mv*)
 
 text \<open>Let \<open>'a\<close> and \<open>'b\<close> be two normed real vector spaces. Then the space of linear continuous
 operators from \<open>'a\<close> to \<open>'b\<close> has a canonical norm, and therefore a canonical corresponding topology
@@ -1196,7 +1196,7 @@
     auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
 
 
-subsection%important \<open>Metrics on product spaces\<close>
+subsection \<open>Metrics on product spaces\<close>
 
 
 text \<open>In general, the product topology is not metrizable, unless the index set is countable.
@@ -1575,7 +1575,7 @@
 
 
 
-subsection%important \<open>Measurability\<close> (*FIX ME move? *)
+subsection \<open>Measurability\<close> (*FIX ME move? *)
 
 text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
 generated by open sets in the product, and the product sigma algebra, countably generated by