subsection is always %important
authorimmler
Thu, 17 Jan 2019 16:38:00 -0500
changeset 69683 8b3458ca0762
parent 69682 500a7acdccd4
child 69684 94284d4dab98
subsection is always %important
src/HOL/Analysis/Arcwise_Connected.thy
src/HOL/Analysis/Binary_Product_Measure.thy
src/HOL/Analysis/Bochner_Integration.thy
src/HOL/Analysis/Borel_Space.thy
src/HOL/Analysis/Caratheodory.thy
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Cartesian_Space.thy
src/HOL/Analysis/Change_Of_Vars.thy
src/HOL/Analysis/Cross3.thy
src/HOL/Analysis/Determinants.thy
src/HOL/Analysis/Elementary_Topology.thy
src/HOL/Analysis/Extended_Real_Limits.thy
src/HOL/Analysis/Fashoda_Theorem.thy
src/HOL/Analysis/Finite_Cartesian_Product.thy
src/HOL/Analysis/Finite_Product_Measure.thy
src/HOL/Analysis/Function_Topology.thy
src/HOL/Analysis/Further_Topology.thy
src/HOL/Analysis/Great_Picard.thy
src/HOL/Analysis/Homeomorphism.thy
src/HOL/Analysis/Improper_Integral.thy
src/HOL/Analysis/Interval_Integral.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Ordered_Euclidean_Space.thy
src/HOL/Analysis/Poly_Roots.thy
src/HOL/Analysis/Polytope.thy
src/HOL/Analysis/Radon_Nikodym.thy
src/HOL/Analysis/Tagged_Division.thy
src/HOL/Analysis/Vitali_Covering_Theorem.thy
src/HOL/Analysis/Weierstrass_Theorems.thy
--- a/src/HOL/Analysis/Arcwise_Connected.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Arcwise_Connected.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -8,7 +8,7 @@
 imports Path_Connected Ordered_Euclidean_Space "HOL-Computational_Algebra.Primes"
 begin
 
-subsection%important \<open>The Brouwer reduction theorem\<close>
+subsection \<open>The Brouwer reduction theorem\<close>
 
 theorem Brouwer_reduction_theorem_gen:
   fixes S :: "'a::euclidean_space set"
@@ -108,7 +108,7 @@
 
 subsection%unimportant\<open>Arcwise Connections\<close>(*FIX ME this subsection is empty(?) *)
 
-subsection%important\<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>.
@@ -2001,7 +2001,7 @@
 
 
 
-subsection%important\<open>Accessibility of frontier points\<close>
+subsection\<open>Accessibility of frontier points\<close>
 
 lemma dense_accessible_frontier_points:
   fixes S :: "'a::{complete_space,real_normed_vector} set"
--- a/src/HOL/Analysis/Binary_Product_Measure.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -14,7 +14,7 @@
 lemma rev_Pair_vimage_times[simp]: "(\<lambda>x. (x, y)) -` (A \<times> B) = (if y \<in> B then A else {})"
   by auto
 
-subsection%important "Binary products"
+subsection "Binary products"
 
 definition%important pair_measure (infixr "\<Otimes>\<^sub>M" 80) where
   "A \<Otimes>\<^sub>M B = measure_of (space A \<times> space B)
@@ -336,7 +336,7 @@
     by (simp add: ac_simps)
 qed
 
-subsection%important \<open>Binary products of \<open>\<sigma>\<close>-finite emeasure spaces\<close>
+subsection \<open>Binary products of \<open>\<sigma>\<close>-finite emeasure spaces\<close>
 
 locale%unimportant pair_sigma_finite = M1?: sigma_finite_measure M1 + M2?: sigma_finite_measure M2
   for M1 :: "'a measure" and M2 :: "'b measure"
@@ -531,7 +531,7 @@
     done
 qed
 
-subsection%important "Fubinis theorem"
+subsection "Fubinis theorem"
 
 lemma measurable_compose_Pair1:
   "x \<in> space M1 \<Longrightarrow> g \<in> measurable (M1 \<Otimes>\<^sub>M M2) L \<Longrightarrow> (\<lambda>y. g (x, y)) \<in> measurable M2 L"
@@ -602,7 +602,7 @@
   shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f x y \<partial>M1) \<partial>M2) = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f x y \<partial>M2) \<partial>M1)"
   using Fubini[OF f] by simp
 
-subsection%important \<open>Products on counting spaces, densities and distributions\<close>
+subsection \<open>Products on counting spaces, densities and distributions\<close>
 
 proposition sigma_prod:
   assumes X_cover: "\<exists>E\<subseteq>A. countable E \<and> X = \<Union>E" and A: "A \<subseteq> Pow X"
@@ -1095,7 +1095,7 @@
 using _ _ assms(1)
 by(rule measurable_compose_countable'[where f="\<lambda>a b. f (a, snd b)" and g=fst and I=A, simplified])simp_all
 
-subsection%important \<open>Product of Borel spaces\<close>
+subsection \<open>Product of Borel spaces\<close>
 
 theorem borel_Times:
   fixes A :: "'a::topological_space set" and B :: "'b::topological_space set"
--- a/src/HOL/Analysis/Bochner_Integration.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -2201,7 +2201,7 @@
   then show ?thesis using \<open>strict_mono r\<close> by auto
 qed
 
-subsection%important \<open>Restricted measure spaces\<close>
+subsection \<open>Restricted measure spaces\<close>
 
 lemma integrable_restrict_space:
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
@@ -2252,7 +2252,7 @@
   thus ?thesis by simp
 qed
 
-subsection%important \<open>Measure spaces with an associated density\<close>
+subsection \<open>Measure spaces with an associated density\<close>
 
 lemma integrable_density:
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"
@@ -2338,7 +2338,7 @@
     has_bochner_integral M (\<lambda>x. g x *\<^sub>R f x) x \<Longrightarrow> has_bochner_integral (density M g) f x"
   by (simp add: has_bochner_integral_iff integrable_density integral_density)
 
-subsection%important \<open>Distributions\<close>
+subsection \<open>Distributions\<close>
 
 lemma integrable_distr_eq:
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
@@ -2410,7 +2410,7 @@
     has_bochner_integral M (\<lambda>x. f (g x)) x \<Longrightarrow> has_bochner_integral (distr M N g) f x"
   by (simp add: has_bochner_integral_iff integrable_distr_eq integral_distr)
 
-subsection%important \<open>Lebesgue integration on \<^const>\<open>count_space\<close>\<close>
+subsection \<open>Lebesgue integration on \<^const>\<open>count_space\<close>\<close>
 
 lemma integrable_count_space:
   fixes f :: "'a \<Rightarrow> 'b::{banach,second_countable_topology}"
@@ -2497,7 +2497,7 @@
   shows "has_bochner_integral (count_space UNIV) f x \<Longrightarrow> f sums x"
   unfolding has_bochner_integral_iff by (auto intro!: sums_integral_count_space_nat)
 
-subsection%important \<open>Point measure\<close>
+subsection \<open>Point measure\<close>
 
 lemma lebesgue_integral_point_measure_finite:
   fixes g :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
@@ -2515,7 +2515,7 @@
   apply (auto simp: AE_count_space integrable_count_space)
   done
 
-subsection%important \<open>Lebesgue integration on \<^const>\<open>null_measure\<close>\<close>
+subsection \<open>Lebesgue integration on \<^const>\<open>null_measure\<close>\<close>
 
 lemma has_bochner_integral_null_measure_iff[iff]:
   "has_bochner_integral (null_measure M) f 0 \<longleftrightarrow> f \<in> borel_measurable M"
@@ -2529,7 +2529,7 @@
   by (cases "integrable (null_measure M) f")
      (auto simp add: not_integrable_integral_eq has_bochner_integral_integral_eq)
 
-subsection%important \<open>Legacy lemmas for the real-valued Lebesgue integral\<close>
+subsection \<open>Legacy lemmas for the real-valued Lebesgue integral\<close>
 theorem real_lebesgue_integral_def:
   assumes f[measurable]: "integrable M f"
   shows "integral\<^sup>L M f = enn2real (\<integral>\<^sup>+x. f x \<partial>M) - enn2real (\<integral>\<^sup>+x. ennreal (- f x) \<partial>M)"
@@ -2839,7 +2839,7 @@
     by (auto simp: _has_bochner_integral_iff)
 qed
 
-subsection%important \<open>Product measure\<close>
+subsection \<open>Product measure\<close>
 
 lemma (in sigma_finite_measure) borel_measurable_lebesgue_integrable[measurable (raw)]:
   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
--- a/src/HOL/Analysis/Borel_Space.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Borel_Space.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -294,7 +294,7 @@
   ultimately show ?thesis using that by blast
 qed
 
-subsection%important \<open>Generic Borel spaces\<close>
+subsection \<open>Generic Borel spaces\<close>
 
 definition%important (in topological_space) borel :: "'a measure" where
   "borel = sigma UNIV {S. open S}"
@@ -669,7 +669,7 @@
     unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
 qed
 
-subsection%important \<open>Borel spaces on order topologies\<close>
+subsection \<open>Borel spaces on order topologies\<close>
 
 lemma [measurable]:
   fixes a b :: "'a::linorder_topology"
@@ -970,7 +970,7 @@
   with u show ?thesis by (simp cong: measurable_cong)
 qed
 
-subsection%important \<open>Borel spaces on topological monoids\<close>
+subsection \<open>Borel spaces on topological monoids\<close>
 
 lemma borel_measurable_add[measurable (raw)]:
   fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, topological_monoid_add}"
@@ -994,7 +994,7 @@
   shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M"
   unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
 
-subsection%important \<open>Borel spaces on Euclidean spaces\<close>
+subsection \<open>Borel spaces on Euclidean spaces\<close>
 
 lemma borel_measurable_inner[measurable (raw)]:
   fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_inner}"
@@ -1329,7 +1329,7 @@
     by (subst borel_measurable_iff_halfspace_le) auto
 qed auto
 
-subsection%important "Borel measurable operators"
+subsection "Borel measurable operators"
 
 lemma borel_measurable_norm[measurable]: "norm \<in> borel_measurable borel"
   by (intro borel_measurable_continuous_on1 continuous_intros)
@@ -1525,7 +1525,7 @@
 lemma measurable_of_bool[measurable]: "of_bool \<in> count_space UNIV \<rightarrow>\<^sub>M borel"
   by simp
 
-subsection%important "Borel space on the extended reals"
+subsection "Borel space on the extended reals"
 
 lemma borel_measurable_ereal[measurable (raw)]:
   assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
@@ -1686,7 +1686,7 @@
   shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M"
   unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
 
-subsection%important "Borel space on the extended non-negative reals"
+subsection "Borel space on the extended non-negative reals"
 
 text \<open> \<^type>\<open>ennreal\<close> is a topological monoid, so no rules for plus are required, also all order
   statements are usually done on type classes. \<close>
@@ -1760,7 +1760,7 @@
 
 hide_const (open) is_borel
 
-subsection%important \<open>LIMSEQ is borel measurable\<close>
+subsection \<open>LIMSEQ is borel measurable\<close>
 
 lemma borel_measurable_LIMSEQ_real:
   fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> real"
--- a/src/HOL/Analysis/Caratheodory.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Caratheodory.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -49,12 +49,12 @@
     by (simp add: suminf_eq_SUP)
 qed
 
-subsection%important \<open>Characterizations of Measures\<close>
+subsection \<open>Characterizations of Measures\<close>
 
 definition%important outer_measure_space where
   "outer_measure_space M f \<longleftrightarrow> positive M f \<and> increasing M f \<and> countably_subadditive M f"
 
-subsubsection%important \<open>Lambda Systems\<close>
+subsubsection \<open>Lambda Systems\<close>
 
 definition%important lambda_system :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a set set"
 where
@@ -460,7 +460,7 @@
 lemma measure_down: "measure_space \<Omega> N \<mu> \<Longrightarrow> sigma_algebra \<Omega> M \<Longrightarrow> M \<subseteq> N \<Longrightarrow> measure_space \<Omega> M \<mu>"
   by (auto simp add: measure_space_def positive_def countably_additive_def subset_eq)
 
-subsection%important \<open>Caratheodory's theorem\<close>
+subsection \<open>Caratheodory's theorem\<close>
 
 theorem (in ring_of_sets) caratheodory':
   assumes posf: "positive M f" and ca: "countably_additive M f"
@@ -497,7 +497,7 @@
   show "\<forall>A\<in>M. f A \<noteq> \<infinity>" using fin by auto
 qed (rule cont)
 
-subsection%important \<open>Volumes\<close>
+subsection \<open>Volumes\<close>
 
 definition%important volume :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
   "volume M f \<longleftrightarrow>
@@ -635,7 +635,7 @@
   qed
 qed
 
-subsubsection%important \<open>Caratheodory on semirings\<close>
+subsubsection \<open>Caratheodory on semirings\<close>
 
 theorem (in semiring_of_sets) caratheodory:
   assumes pos: "positive M \<mu>" and ca: "countably_additive M \<mu>"
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -45,7 +45,7 @@
         "box (vec a) (vec b) = {} \<longleftrightarrow> box a b = {}"
   by (auto simp: Basis_vec_def mem_box box_eq_empty inner_axis)
 
-subsection%important\<open>Closures and interiors of halfspaces\<close>
+subsection\<open>Closures and interiors of halfspaces\<close>
 
 lemma%important interior_halfspace_le [simp]:
   assumes "a \<noteq> 0"
@@ -190,7 +190,7 @@
   by (simp_all add: linear_continuous_at linear_continuous_on)
 
 
-subsection%important\<open>Bounds on components etc.\ relative to operator norm\<close>
+subsection\<open>Bounds on components etc.\ relative to operator norm\<close>
 
 lemma%important norm_column_le_onorm:
   fixes A :: "real^'n^'m"
@@ -527,7 +527,7 @@
     unfolding Collect_all_eq by (simp add: closed_INT)
 qed
 
-subsection%important "Convex Euclidean Space"
+subsection "Convex Euclidean Space"
 
 lemma%unimportant Cart_1:"(1::real^'n) = \<Sum>Basis"
   using const_vector_cart[of 1] by (simp add: one_vec_def)
@@ -563,7 +563,7 @@
 qed
 
 
-subsection%important "Derivative"
+subsection "Derivative"
 
 definition%important "jacobian f net = matrix(frechet_derivative f net)"
 
--- a/src/HOL/Analysis/Cartesian_Space.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Cartesian_Space.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -501,7 +501,7 @@
 qed
 
 
-subsection%important\<open> Rank of a matrix\<close>
+subsection\<open> Rank of a matrix\<close>
 
 text\<open>Equivalence of row and column rank is taken from George Mackiw's paper, Mathematics Magazine 1995, p. 285.\<close>
 
@@ -942,7 +942,7 @@
   by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
 
 
-subsection%important  \<open>Orthogonality of a matrix\<close>
+subsection  \<open>Orthogonality of a matrix\<close>
 
 definition%important  "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow>
   transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
@@ -1008,7 +1008,7 @@
 qed
 
 
-subsection%important \<open> We can find an orthogonal matrix taking any unit vector to any other\<close>
+subsection \<open> We can find an orthogonal matrix taking any unit vector to any other\<close>
 
 lemma%unimportant  orthogonal_matrix_transpose [simp]:
      "orthogonal_matrix(transpose A) \<longleftrightarrow> orthogonal_matrix A"
@@ -1103,7 +1103,7 @@
 qed
 
 
-subsection%important  \<open>Linearity of scaling, and hence isometry, that preserves origin\<close>
+subsection  \<open>Linearity of scaling, and hence isometry, that preserves origin\<close>
 
 lemma%important  scaling_linear:
   fixes f :: "'a::real_inner \<Rightarrow> 'a::real_inner"
@@ -1138,7 +1138,7 @@
   by (metis dist_0_norm)
 
 
-subsection%important  \<open>Can extend an isometry from unit sphere\<close>
+subsection  \<open>Can extend an isometry from unit sphere\<close>
 
 lemma%important  isometry_sphere_extend:
   fixes f:: "'a::real_inner \<Rightarrow> 'a"
@@ -1178,7 +1178,7 @@
     by (rule exI[where x= ?g]) (metis thfg thd)
 qed
 
-subsection%important\<open>Induction on matrix row operations\<close>
+subsection\<open>Induction on matrix row operations\<close>
 
 lemma%unimportant induct_matrix_row_operations:
   fixes P :: "real^'n^'n \<Rightarrow> bool"
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -421,7 +421,7 @@
     by (simp add: measure_linear_image \<open>linear f\<close> S f)
 qed
 
-subsection%important\<open>\<open>F_sigma\<close> and \<open>G_delta\<close> sets.\<close>(*FIX ME mv *)
+subsection\<open>\<open>F_sigma\<close> and \<open>G_delta\<close> sets.\<close>(*FIX ME mv *)
 
 (*https://en.wikipedia.org/wiki/F\<sigma>_set*)
 inductive%important fsigma :: "'a::topological_space set \<Rightarrow> bool" where
@@ -1411,7 +1411,7 @@
     by (blast intro: order_trans)
 qed
 
-subsection%important\<open>Borel measurable Jacobian determinant\<close>
+subsection\<open>Borel measurable Jacobian determinant\<close>
 
 lemma%unimportant lemma_partial_derivatives0:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -2184,7 +2184,7 @@
 qed
 
 
-subsection%important\<open>Simplest case of Sard's theorem (we don't need continuity of derivative)\<close>
+subsection\<open>Simplest case of Sard's theorem (we don't need continuity of derivative)\<close>
 
 lemma%important Sard_lemma00:
   fixes P :: "'b::euclidean_space set"
@@ -2547,7 +2547,7 @@
 qed
 
 
-subsection%important\<open>A one-way version of change-of-variables not assuming injectivity. \<close>
+subsection\<open>A one-way version of change-of-variables not assuming injectivity. \<close>
 
 lemma%important integral_on_image_ubound_weak:
   fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real"
@@ -2960,7 +2960,7 @@
   using%unimportant integral_on_image_ubound_nonneg [OF assms] by%unimportant simp
 
 
-subsection%important\<open>Change-of-variables theorem\<close>
+subsection\<open>Change-of-variables theorem\<close>
 
 text\<open>The classic change-of-variables theorem. We have two versions with quite general hypotheses,
 the first that the transforming function has a continuous inverse, the second that the base set is
@@ -3638,7 +3638,7 @@
   using%unimportant has_absolute_integral_change_of_variables_1 [OF assms] by%unimportant auto
 
 
-subsection%important\<open>Change of variables for integrals: special case of linear function\<close>
+subsection\<open>Change of variables for integrals: special case of linear function\<close>
 
 lemma%unimportant has_absolute_integral_change_of_variables_linear:
   fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_"
@@ -3697,7 +3697,7 @@
     by blast
 qed
 
-subsection%important\<open>Change of variable for measure\<close>
+subsection\<open>Change of variable for measure\<close>
 
 lemma%unimportant has_measure_differentiable_image:
   fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_"
--- a/src/HOL/Analysis/Cross3.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Cross3.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -33,7 +33,7 @@
 
 unbundle cross3_syntax
 
-subsection%important\<open> Basic lemmas\<close>
+subsection\<open> Basic lemmas\<close>
 
 lemmas cross3_simps = cross3_def inner_vec_def sum_3 det_3 vec_eq_iff vector_def algebra_simps
 
@@ -168,7 +168,7 @@
   apply (simp add: cross_mult_left)
   done
 
-subsection%important   \<open>Preservation by rotation, or other orthogonal transformation up to sign\<close>
+subsection   \<open>Preservation by rotation, or other orthogonal transformation up to sign\<close>
 
 lemma  cross_matrix_mult: "transpose A *v ((A *v x) \<times> (A *v y)) = det A *\<^sub>R (x \<times> y)"
   apply (simp add: vec_eq_iff   )
@@ -208,7 +208,7 @@
            \<Longrightarrow> (f x) \<times> (f y) = f(x \<times> y)"
   by (simp add: cross_orthogonal_transformation orthogonal_transformation)
 
-subsection%important \<open>Continuity\<close>
+subsection \<open>Continuity\<close>
 
 lemma  continuous_cross: "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. (f x) \<times> (g x))"
   apply (subst continuous_componentwise)
--- a/src/HOL/Analysis/Determinants.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Determinants.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -10,7 +10,7 @@
   "HOL-Library.Permutations"
 begin
 
-subsection%important  \<open>Trace\<close>
+subsection  \<open>Trace\<close>
 
 definition%important  trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a"
   where "trace A = sum (\<lambda>i. ((A$i)$i)) (UNIV::'n set)"
@@ -33,7 +33,7 @@
   apply (simp add: mult.commute)
   done
 
-subsubsection%important  \<open>Definition of determinant\<close>
+subsubsection  \<open>Definition of determinant\<close>
 
 definition%important  det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where
   "det A =
@@ -712,7 +712,7 @@
 qed
 
 
-subsection%important \<open>Relation to invertibility\<close>
+subsection \<open>Relation to invertibility\<close>
 
 lemma%important  invertible_det_nz:
   fixes A::"'a::{field}^'n^'n"
@@ -776,7 +776,7 @@
   using invertible_det_nz [of A]
   by (auto simp: matrix_left_invertible_injective invertible_left_inverse less_rank_noninjective)
 
-subsubsection%important  \<open>Invertibility of matrices and corresponding linear functions\<close>
+subsubsection  \<open>Invertibility of matrices and corresponding linear functions\<close>
 
 lemma%important  matrix_left_invertible_gen:
   fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n"
@@ -861,7 +861,7 @@
       vec.linear_injective_left_inverse vec.linear_surjective_right_inverse)
 
 
-subsection%important \<open>Cramer's rule\<close>
+subsection \<open>Cramer's rule\<close>
 
 lemma%important  cramer_lemma_transpose:
   fixes A:: "'a::{field}^'n^'n"
@@ -996,7 +996,7 @@
   shows "orthogonal_transformation f \<Longrightarrow> \<bar>det (matrix f)\<bar> = 1"
   using%unimportant det_orthogonal_matrix orthogonal_transformation_matrix by fastforce
 
-subsection%important  \<open>Rotation, reflection, rotoinversion\<close>
+subsection  \<open>Rotation, reflection, rotoinversion\<close>
 
 definition%important  "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
 definition%important  "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
--- a/src/HOL/Analysis/Elementary_Topology.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -650,7 +650,7 @@
 qed
 
 
-subsection%important \<open>Polish spaces\<close>
+subsection \<open>Polish spaces\<close>
 
 text \<open>Textbooks define Polish spaces as completely metrizable.
   We assume the topology to be complete for a given metric.\<close>
--- a/src/HOL/Analysis/Extended_Real_Limits.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -357,7 +357,7 @@
   done
 
 
-subsection%important \<open>Extended-Real.thy\<close> (*FIX ME change title *)
+subsection \<open>Extended-Real.thy\<close> (*FIX ME change title *)
 
 lemma sum_constant_ereal:
   fixes a::ereal
@@ -391,7 +391,7 @@
 qed
 
 
-subsubsection%important \<open>Continuity of addition\<close>
+subsubsection \<open>Continuity of addition\<close>
 
 text \<open>The next few lemmas remove an unnecessary assumption in \<open>tendsto_add_ereal\<close>, culminating
 in \<open>tendsto_add_ereal_general\<close> which essentially says that the addition
@@ -522,7 +522,7 @@
   then show ?thesis using tendsto_add_ereal_MInf MInf f g by (metis ereal_MInfty_eq_plus)
 qed
 
-subsubsection%important \<open>Continuity of multiplication\<close>
+subsubsection \<open>Continuity of multiplication\<close>
 
 text \<open>In the same way as for addition, we prove that the multiplication is continuous on
 ereal times ereal, except at \<open>(\<infinity>, 0)\<close> and \<open>(-\<infinity>, 0)\<close> and \<open>(0, \<infinity>)\<close> and \<open>(0, -\<infinity>)\<close>,
@@ -659,7 +659,7 @@
 by (cases "c = 0", auto simp add: assms tendsto_mult_ereal)
 
 
-subsubsection%important \<open>Continuity of division\<close>
+subsubsection \<open>Continuity of division\<close>
 
 lemma tendsto_inverse_ereal_PInf:
   fixes u::"_ \<Rightarrow> ereal"
@@ -762,7 +762,7 @@
 qed
 
 
-subsubsection%important \<open>Further limits\<close>
+subsubsection \<open>Further limits\<close>
 
 text \<open>The assumptions of @{thm tendsto_diff_ereal} are too strong, we weaken them here.\<close>
 
@@ -958,7 +958,7 @@
 by (subst uminus_ereal.simps(1)[symmetric], intro tendsto_intros)
 
 
-subsection%important \<open>Extended-Nonnegative-Real.thy\<close> (*FIX title *)
+subsection \<open>Extended-Nonnegative-Real.thy\<close> (*FIX title *)
 
 lemma tendsto_diff_ennreal_general [tendsto_intros]:
   fixes u v::"'a \<Rightarrow> ennreal"
@@ -987,7 +987,7 @@
 qed
 
 
-subsection%important \<open>monoset\<close> (*FIX ME title *)
+subsection \<open>monoset\<close> (*FIX ME title *)
 
 definition (in order) mono_set:
   "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
@@ -1759,7 +1759,7 @@
     by (auto simp: * ereal_diff_positive max.absorb2 liminf_SUP_INF[symmetric] limsup_INF_SUP[symmetric] ereal_liminf_limsup_minus)
 qed
 
-subsection%important "Relate extended reals and the indicator function"
+subsection "Relate extended reals and the indicator function"
 
 lemma ereal_indicator_le_0: "(indicator S x::ereal) \<le> 0 \<longleftrightarrow> x \<notin> S"
   by (auto split: split_indicator simp: one_ereal_def)
--- a/src/HOL/Analysis/Fashoda_Theorem.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Fashoda_Theorem.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -8,7 +8,7 @@
 imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
 begin
 
-subsection%important \<open>Bijections between intervals\<close>
+subsection \<open>Bijections between intervals\<close>
 
 definition%important interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space"
   where "interval_bij =
@@ -70,7 +70,7 @@
   using assms by (intro interval_bij_bij) (auto simp: Basis_vec_def inner_axis)
 
 
-subsection%important \<open>Fashoda meet theorem\<close>
+subsection \<open>Fashoda meet theorem\<close>
 
 lemma infnorm_2:
   fixes x :: "real^2"
@@ -630,7 +630,7 @@
 qed
 
 
-subsection%important \<open>Useful Fashoda corollary pointed out to me by Tom Hales\<close>(*FIXME change title? *)
+subsection \<open>Useful Fashoda corollary pointed out to me by Tom Hales\<close>(*FIXME change title? *)
 
 corollary fashoda_interlace:
   fixes a :: "real^2"
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -68,7 +68,7 @@
 lemma vec_lambda_eta [simp]: "(\<chi> i. (g$i)) = g"
   by (simp add: vec_eq_iff)
 
-subsection%important \<open>Cardinality of vectors\<close>
+subsection \<open>Cardinality of vectors\<close>
 
 instance vec :: (finite, finite) finite
 proof
@@ -292,7 +292,7 @@
   "scalar_product v w = (\<Sum> i \<in> UNIV. v $ i * w $ i)"
 
 
-subsection%important \<open>Real vector space\<close>
+subsection \<open>Real vector space\<close>
 
 instantiation%unimportant vec :: (real_vector, finite) real_vector
 begin
@@ -308,7 +308,7 @@
 end
 
 
-subsection%important \<open>Topological space\<close>
+subsection \<open>Topological space\<close>
 
 instantiation%unimportant vec :: (topological_space, finite) topological_space
 begin
@@ -430,7 +430,7 @@
 qed
 
 
-subsection%important \<open>Metric space\<close>
+subsection \<open>Metric space\<close>
 (* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
 
 instantiation%unimportant vec :: (metric_space, finite) dist
@@ -570,7 +570,7 @@
 qed
 
 
-subsection%important \<open>Normed vector space\<close>
+subsection \<open>Normed vector space\<close>
 
 instantiation%unimportant vec :: (real_normed_vector, finite) real_normed_vector
 begin
@@ -636,7 +636,7 @@
 instance vec :: (banach, finite) banach ..
 
 
-subsection%important \<open>Inner product space\<close>
+subsection \<open>Inner product space\<close>
 
 instantiation%unimportant vec :: (real_inner, finite) real_inner
 begin
@@ -668,7 +668,7 @@
 end
 
 
-subsection%important \<open>Euclidean space\<close>
+subsection \<open>Euclidean space\<close>
 
 text \<open>Vectors pointing along a single axis.\<close>
 
@@ -992,7 +992,7 @@
   apply (auto )
   by unfold_locales (vector algebra_simps)+
 
-subsection%important \<open>Matrix operations\<close>
+subsection \<open>Matrix operations\<close>
 
 text\<open>Matrix notation. NB: an MxN matrix is of type \<^typ>\<open>'a^'n^'m\<close>, not \<^typ>\<open>'a^'m^'n\<close>\<close>
 
@@ -1202,7 +1202,7 @@
   "(A::'a::comm_semiring_1^'n^_) *v x = sum (\<lambda>i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)"
   by (simp add: matrix_vector_mult_def transpose_def vec_eq_iff mult.commute)
 
-subsection%important\<open>Inverse matrices  (not necessarily square)\<close>
+subsection\<open>Inverse matrices  (not necessarily square)\<close>
 
 definition%important
   "invertible(A::'a::semiring_1^'n^'m) \<longleftrightarrow> (\<exists>A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
--- a/src/HOL/Analysis/Finite_Product_Measure.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -109,9 +109,9 @@
   "I \<inter> J = {} \<Longrightarrow> merge I J -` Pi\<^sub>E (I \<union> J) E = Pi I E \<times> Pi J E"
   by (auto simp: restrict_Pi_cancel PiE_def)
 
-subsection%important \<open>Finite product spaces\<close>
+subsection \<open>Finite product spaces\<close>
 
-subsubsection%important \<open>Products\<close>
+subsubsection \<open>Products\<close>
 
 definition%important prod_emb where
   "prod_emb I M K X = (\<lambda>x. restrict x K) -` X \<inter> (\<Pi>\<^sub>E i\<in>I. space (M i))"
--- 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
--- a/src/HOL/Analysis/Further_Topology.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Further_Topology.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -6,7 +6,7 @@
   imports Equivalence_Lebesgue_Henstock_Integration Weierstrass_Theorems Polytope Complex_Transcendental
 begin
 
-subsection%important\<open>A map from a sphere to a higher dimensional sphere is nullhomotopic\<close>
+subsection\<open>A map from a sphere to a higher dimensional sphere is nullhomotopic\<close>
 
 lemma spheremap_lemma1:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
@@ -377,7 +377,7 @@
 
 
 
-subsection%important\<open> Some technical lemmas about extending maps from cell complexes\<close>
+subsection\<open> Some technical lemmas about extending maps from cell complexes\<close>
 
 lemma extending_maps_Union_aux:
   assumes fin: "finite \<F>"
@@ -991,7 +991,7 @@
 
 
 
-subsection%important\<open> Special cases and corollaries involving spheres\<close>
+subsection\<open> Special cases and corollaries involving spheres\<close>
 
 lemma disjnt_Diff1: "X \<subseteq> Y' \<Longrightarrow> disjnt (X - Y) (X' - Y')"
   by (auto simp: disjnt_def)
@@ -1140,7 +1140,7 @@
     by (rule_tac K="K \<inter> T" and g=g in that) (auto simp: disjnt_iff Diff_Int contg)
 qed
 
-subsection%important\<open>Extending maps to spheres\<close>
+subsection\<open>Extending maps to spheres\<close>
 
 (*Up to extend_map_affine_to_sphere_cofinite_gen*)
 
@@ -1892,7 +1892,7 @@
     done
 qed
 
-subsection%important\<open> Invariance of domain and corollaries\<close>
+subsection\<open> Invariance of domain and corollaries\<close>
 
 lemma invariance_of_domain_ball:
   fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
@@ -2742,7 +2742,7 @@
     using clopen [of S] False  by simp
 qed
 
-subsection%important\<open>Dimension-based conditions for various homeomorphisms\<close>
+subsection\<open>Dimension-based conditions for various homeomorphisms\<close>
 
 lemma homeomorphic_subspaces_eq:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
@@ -2819,7 +2819,7 @@
   qed
 qed
 
-subsection%important\<open>more invariance of domain\<close>(*FIX ME title? *)
+subsection\<open>more invariance of domain\<close>(*FIX ME title? *)
 
 proposition invariance_of_domain_sphere_affine_set_gen:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -3114,7 +3114,7 @@
 qed
 
 
-subsection%important\<open>The power, squaring and exponential functions as covering maps\<close>
+subsection\<open>The power, squaring and exponential functions as covering maps\<close>
 
 proposition covering_space_power_punctured_plane:
   assumes "0 < n"
@@ -3487,7 +3487,7 @@
 qed
 
 
-subsection%important\<open>Hence the Borsukian results about mappings into circles\<close>(*FIX ME title *)
+subsection\<open>Hence the Borsukian results about mappings into circles\<close>(*FIX ME title *)
 
 lemma inessential_eq_continuous_logarithm:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
@@ -3637,7 +3637,7 @@
     by (simp add: *)
 qed
 
-subsection%important\<open>Upper and lower hemicontinuous functions\<close>
+subsection\<open>Upper and lower hemicontinuous functions\<close>
 
 text\<open>And relation in the case of preimage map to open and closed maps, and fact that upper and lower
 hemicontinuity together imply continuity in the sense of the Hausdorff metric (at points where the
@@ -3840,7 +3840,7 @@
 qed
 
 
-subsection%important\<open>Complex logs exist on various "well-behaved" sets\<close>
+subsection\<open>Complex logs exist on various "well-behaved" sets\<close>
 
 lemma continuous_logarithm_on_contractible:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
@@ -3909,7 +3909,7 @@
 qed
 
 
-subsection%important\<open>Another simple case where sphere maps are nullhomotopic\<close>
+subsection\<open>Another simple case where sphere maps are nullhomotopic\<close>
 
 lemma inessential_spheremap_2_aux:
   fixes f :: "'a::euclidean_space \<Rightarrow> complex"
@@ -3975,7 +3975,7 @@
 qed
 
 
-subsection%important\<open>Holomorphic logarithms and square roots\<close>
+subsection\<open>Holomorphic logarithms and square roots\<close>
 
 lemma contractible_imp_holomorphic_log:
   assumes holf: "f holomorphic_on S"
@@ -4189,7 +4189,7 @@
 qed
 
 
-subsection%important\<open>The "Borsukian" property of sets\<close>
+subsection\<open>The "Borsukian" property of sets\<close>
 
 text\<open>This doesn't have a standard name. Kuratowski uses ``contractible with respect to \<open>[S\<^sup>1]\<close>''
  while Whyburn uses ``property b''. It's closely related to unicoherence.\<close>
@@ -4807,7 +4807,7 @@
 qed
 
 
-subsection%important\<open>Unicoherence (closed)\<close>
+subsection\<open>Unicoherence (closed)\<close>
 
 definition%important unicoherent where
   "unicoherent U \<equiv>
@@ -5051,7 +5051,7 @@
 qed
 
 
-subsection%important\<open>Several common variants of unicoherence\<close>
+subsection\<open>Several common variants of unicoherence\<close>
 
 lemma connected_frontier_simple:
   fixes S :: "'a :: euclidean_space set"
@@ -5104,7 +5104,7 @@
 qed
 
 
-subsection%important\<open>Some separation results\<close>
+subsection\<open>Some separation results\<close>
 
 lemma separation_by_component_closed_pointwise:
   fixes S :: "'a :: euclidean_space set"
--- a/src/HOL/Analysis/Great_Picard.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Great_Picard.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -374,7 +374,7 @@
 qed
 
   
-subsection%important\<open>The Little Picard Theorem\<close>
+subsection\<open>The Little Picard Theorem\<close>
 
 proposition Landau_Picard:
   obtains R
@@ -614,7 +614,7 @@
 qed
 
 
-subsection%important\<open>The ArzelĂ --Ascoli theorem\<close>
+subsection\<open>The ArzelĂ --Ascoli theorem\<close>
 
 lemma subsequence_diagonalization_lemma:
   fixes P :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"
@@ -788,7 +788,7 @@
 
 
 
-subsubsection%important\<open>Montel's theorem\<close>
+subsubsection\<open>Montel's theorem\<close>
 
 text\<open>a sequence of holomorphic functions uniformly bounded
 on compact subsets of an open set S has a subsequence that converges to a
@@ -993,7 +993,7 @@
 
 
 
-subsection%important\<open>Some simple but useful cases of Hurwitz's theorem\<close>
+subsection\<open>Some simple but useful cases of Hurwitz's theorem\<close>
 
 proposition Hurwitz_no_zeros:
   assumes S: "open S" "connected S"
@@ -1229,7 +1229,7 @@
 
 
 
-subsection%important\<open>The Great Picard theorem\<close>
+subsection\<open>The Great Picard theorem\<close>
 
 lemma GPicard1:
   assumes S: "open S" "connected S" and "w \<in> S" "0 < r" "Y \<subseteq> X"
--- a/src/HOL/Analysis/Homeomorphism.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Homeomorphism.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -36,7 +36,7 @@
   using assms  apply auto
   done
 
-subsection%important \<open>Homeomorphism of all convex compact sets with nonempty interior\<close>
+subsection \<open>Homeomorphism of all convex compact sets with nonempty interior\<close>
 
 proposition ray_to_rel_frontier:
   fixes a :: "'a::real_inner"
@@ -725,7 +725,7 @@
 by (simp add: rel_frontier_def convex_rel_interior_closure)
 
 
-subsection%important\<open>Homeomorphisms between punctured spheres and affine sets\<close>
+subsection\<open>Homeomorphisms between punctured spheres and affine sets\<close>
 text\<open>Including the famous stereoscopic projection of the 3-D sphere to the complex plane\<close>
 
 text\<open>The special case with centre 0 and radius 1\<close>
@@ -1004,7 +1004,7 @@
     done
 qed
 
-subsection%important\<open>Locally compact sets in an open set\<close>
+subsection\<open>Locally compact sets in an open set\<close>
 
 text\<open> Locally compact sets are closed in an open set and are homeomorphic
   to an absolutely closed set if we have one more dimension to play with.\<close>
@@ -1995,7 +1995,7 @@
     done
 qed
 
-subsection%important\<open> Lifting of general functions to covering space\<close>
+subsection\<open> Lifting of general functions to covering space\<close>
 
 proposition covering_space_lift_path_strong:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
--- a/src/HOL/Analysis/Improper_Integral.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Improper_Integral.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -4,7 +4,7 @@
   imports Equivalence_Lebesgue_Henstock_Integration
 begin
 
-subsection%important \<open>Equiintegrability\<close>
+subsection \<open>Equiintegrability\<close>
 
 text\<open>The definition here only really makes sense for an elementary set. 
      We just use compact intervals in applications below.\<close>
@@ -226,7 +226,7 @@
     by auto 
 qed
 
-subsection%important\<open>Subinterval restrictions for equiintegrable families\<close>
+subsection\<open>Subinterval restrictions for equiintegrable families\<close>
 
 text\<open>First, some technical lemmas about minimizing a "flat" part of a sum over a division.\<close>
 
@@ -1264,7 +1264,7 @@
   
 
 
-subsection%important\<open>Continuity of the indefinite integral\<close>
+subsection\<open>Continuity of the indefinite integral\<close>
 
 proposition indefinite_integral_continuous:
   fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
--- a/src/HOL/Analysis/Interval_Integral.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Interval_Integral.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -37,7 +37,7 @@
 lemma borel_einterval[measurable]: "einterval a b \<in> sets borel"
   unfolding einterval_def by measurable
 
-subsection%important \<open>Approximating a (possibly infinite) interval\<close>
+subsection \<open>Approximating a (possibly infinite) interval\<close>
 
 lemma filterlim_sup1: "(LIM x F. f x :> G1) \<Longrightarrow> (LIM x F. f x :> (sup G1 G2))"
  unfolding filterlim_def by (auto intro: le_supI1)
@@ -151,7 +151,7 @@
 translations
   "LBINT x=a..b. f" == "CONST interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
 
-subsection%important\<open>Basic properties of integration over an interval\<close>
+subsection\<open>Basic properties of integration over an interval\<close>
 
 lemma interval_lebesgue_integral_cong:
   "a \<le> b \<Longrightarrow> (\<And>x. x \<in> einterval a b \<Longrightarrow> f x = g x) \<Longrightarrow> einterval a b \<in> sets M \<Longrightarrow>
@@ -303,7 +303,7 @@
   (set_integrable M {a<..} f)"
   unfolding%unimportant interval_lebesgue_integrable_def by auto
 
-subsection%important\<open>Basic properties of integration over an interval wrt lebesgue measure\<close>
+subsection\<open>Basic properties of integration over an interval wrt lebesgue measure\<close>
 
 lemma interval_integral_zero [simp]:
   fixes a b :: ereal
@@ -476,7 +476,7 @@
   by (subst interval_lebesgue_integral_le_eq, simp) (rule set_borel_integral_eq_integral)
 
 
-subsection%important\<open>General limit approximation arguments\<close>
+subsection\<open>General limit approximation arguments\<close>
 
 proposition interval_integral_Icc_approx_nonneg:
   fixes a b :: ereal
@@ -571,7 +571,7 @@
     by (simp add: interval_lebesgue_integral_le_eq[symmetric] interval_integral_Icc less_imp_le)
 qed
 
-subsection%important\<open>A slightly stronger Fundamental Theorem of Calculus\<close>
+subsection\<open>A slightly stronger Fundamental Theorem of Calculus\<close>
 
 text\<open>Three versions: first, for finite intervals, and then two versions for
     arbitrary intervals.\<close>
@@ -781,7 +781,7 @@
   qed
 qed
 
-subsection%important\<open>The substitution theorem\<close>
+subsection\<open>The substitution theorem\<close>
 
 text\<open>Once again, three versions: first, for finite intervals, and then two versions for
     arbitrary intervals.\<close>
--- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -297,7 +297,7 @@
 qed
 
 
-subsection%important  \<open>Orthogonality of a transformation\<close>
+subsection  \<open>Orthogonality of a transformation\<close>
 
 definition%important  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
 
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -1,4 +1,4 @@
-subsection%important \<open>Ordered Euclidean Space\<close>
+subsection \<open>Ordered Euclidean Space\<close>
 
 theory Ordered_Euclidean_Space
 imports
--- a/src/HOL/Analysis/Poly_Roots.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Poly_Roots.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -8,7 +8,7 @@
 imports Complex_Main
 begin
 
-subsection%important\<open>Basics about polynomial functions: extremal behaviour and root counts\<close>
+subsection\<open>Basics about polynomial functions: extremal behaviour and root counts\<close>
 
 lemma%important sub_polyfun:
   fixes x :: "'a::{comm_ring,monoid_mult}"
--- a/src/HOL/Analysis/Polytope.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Polytope.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -6,7 +6,7 @@
 imports Cartesian_Euclidean_Space
 begin
 
-subsection%important \<open>Faces of a (usually convex) set\<close>
+subsection \<open>Faces of a (usually convex) set\<close>
 
 definition%important face_of :: "['a::real_vector set, 'a set] \<Rightarrow> bool" (infixr "(face'_of)" 50)
   where
@@ -641,7 +641,7 @@
          F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<ge> b}"
 using face_of_halfspace_le [of F "-a" "-b"] by simp
 
-subsection%important\<open>Exposed faces\<close>
+subsection\<open>Exposed faces\<close>
 
 text\<open>That is, faces that are intersection with supporting hyperplane\<close>
 
@@ -874,7 +874,7 @@
     unfolding exposed_face_of_def by blast
 qed
 
-subsection%important\<open>Extreme points of a set: its singleton faces\<close>
+subsection\<open>Extreme points of a set: its singleton faces\<close>
 
 definition%important extreme_point_of :: "['a::real_vector, 'a set] \<Rightarrow> bool"
                                (infixr "(extreme'_point'_of)" 50)
@@ -974,7 +974,7 @@
 apply (auto simp: face_of_singleton hull_same)
 done
 
-subsection%important\<open>Facets\<close>
+subsection\<open>Facets\<close>
 
 definition%important facet_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
                     (infixr "(facet'_of)" 50)
@@ -1020,7 +1020,7 @@
     "F facet_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
 using facet_of_halfspace_le [of F "-a" "-b"] by simp
 
-subsection%important \<open>Edges: faces of affine dimension 1\<close>
+subsection \<open>Edges: faces of affine dimension 1\<close>
 
 definition%important edge_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"  (infixr "(edge'_of)" 50)
   where "e edge_of S \<longleftrightarrow> e face_of S \<and> aff_dim e = 1"
@@ -1029,7 +1029,7 @@
    "S edge_of T \<Longrightarrow> S \<subseteq> T"
 by (simp add: edge_of_def face_of_imp_subset)
 
-subsection%important\<open>Existence of extreme points\<close>
+subsection\<open>Existence of extreme points\<close>
 
 lemma%important different_norm_3_collinear_points:
   fixes a :: "'a::euclidean_space"
@@ -1105,7 +1105,7 @@
     done
 qed
 
-subsection%important\<open>Krein-Milman, the weaker form\<close>
+subsection\<open>Krein-Milman, the weaker form\<close>
 
 proposition%important Krein_Milman:
   fixes S :: "'a::euclidean_space set"
@@ -1231,7 +1231,7 @@
 qed
 
 
-subsection%important\<open>Applying it to convex hulls of explicitly indicated finite sets\<close>
+subsection\<open>Applying it to convex hulls of explicitly indicated finite sets\<close>
 
 lemma%important Krein_Milman_polytope:
   fixes S :: "'a::euclidean_space set"
@@ -1599,7 +1599,7 @@
   finally show "?rhs \<subseteq> ?lhs" .
 qed
 
-subsection%important\<open>Polytopes\<close>
+subsection\<open>Polytopes\<close>
 
 definition%important polytope where
  "polytope S \<equiv> \<exists>v. finite v \<and> S = convex hull v"
@@ -1694,7 +1694,7 @@
 qed
 
 
-subsection%important\<open>Polyhedra\<close>
+subsection\<open>Polyhedra\<close>
 
 definition%important polyhedron where
  "polyhedron S \<equiv>
@@ -1787,7 +1787,7 @@
 by (simp add: affine_imp_polyhedron)
 
 
-subsection%important\<open>Canonical polyhedron representation making facial structure explicit\<close>
+subsection\<open>Canonical polyhedron representation making facial structure explicit\<close>
 
 lemma%important polyhedron_Int_affine:
   fixes S :: "'a :: euclidean_space set"
@@ -2689,7 +2689,7 @@
   by (subst polyhedron_linear_image_eq)
     (auto simp: bij_uminus intro!: linear_uminus)
 
-subsection%important\<open>Relation between polytopes and polyhedra\<close>
+subsection\<open>Relation between polytopes and polyhedra\<close>
 
 lemma%important polytope_eq_bounded_polyhedron:
   fixes S :: "'a :: euclidean_space set"
@@ -2755,7 +2755,7 @@
 by (simp add: polytope_convex_hull polytope_imp_polyhedron)
 
 
-subsection%important\<open>Relative and absolute frontier of a polytope\<close>
+subsection\<open>Relative and absolute frontier of a polytope\<close>
 
 lemma rel_boundary_of_convex_hull:
     fixes S :: "'a::euclidean_space set"
@@ -3208,7 +3208,7 @@
   qed (use C in auto)
 qed
 
-subsection%important \<open>Simplicial complexes and triangulations\<close>
+subsection \<open>Simplicial complexes and triangulations\<close>
 
 definition%important simplicial_complex where
  "simplicial_complex \<C> \<equiv>
@@ -3226,7 +3226,7 @@
                 \<longrightarrow> (T \<inter> T') face_of T \<and> (T \<inter> T') face_of T')"
 
 
-subsection%important\<open>Refining a cell complex to a simplicial complex\<close>
+subsection\<open>Refining a cell complex to a simplicial complex\<close>
 
 lemma%important convex_hull_insert_Int_eq:
   fixes z :: "'a :: euclidean_space"
@@ -3894,7 +3894,7 @@
   qed
 qed
 
-subsection%important\<open>Some results on cell division with full-dimensional cells only\<close>
+subsection\<open>Some results on cell division with full-dimensional cells only\<close>
 
 lemma%important convex_Union_fulldim_cells:
   assumes "finite \<S>" and clo: "\<And>C. C \<in> \<S> \<Longrightarrow> closed C" and con: "\<And>C. C \<in> \<S> \<Longrightarrow> convex C"
--- a/src/HOL/Analysis/Radon_Nikodym.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Radon_Nikodym.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -163,7 +163,7 @@
   qed measurable
 qed
 
-subsection%important "Absolutely continuous"
+subsection "Absolutely continuous"
 
 definition%important absolutely_continuous :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
   "absolutely_continuous M N \<longleftrightarrow> null_sets M \<subseteq> null_sets N"
@@ -198,7 +198,7 @@
   qed
 qed
 
-subsection%important "Existence of the Radon-Nikodym derivative"
+subsection "Existence of the Radon-Nikodym derivative"
 
 lemma%important
  (in finite_measure) Radon_Nikodym_finite_measure:
@@ -607,7 +607,7 @@
     by (auto intro!: bexI[of _ "\<lambda>x. h x * f x"] simp: density_density_eq)
 qed
 
-subsection%important \<open>Uniqueness of densities\<close>
+subsection \<open>Uniqueness of densities\<close>
 
 lemma%important finite_density_unique:
   assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
@@ -887,7 +887,7 @@
   by (subst sigma_finite_iff_density_finite')
      (auto simp: max_def intro!: measurable_If)
 
-subsection%important \<open>Radon-Nikodym derivative\<close>
+subsection \<open>Radon-Nikodym derivative\<close>
 
 definition%important RN_deriv :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a \<Rightarrow> ennreal" where
   "RN_deriv M N =
--- a/src/HOL/Analysis/Tagged_Division.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Tagged_Division.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -55,7 +55,7 @@
     by (simp add: field_simps)
 qed
 
-subsection%important \<open>Some useful lemmas about intervals\<close>
+subsection \<open>Some useful lemmas about intervals\<close>
 
 lemma interior_subset_union_intervals:
   assumes "i = cbox a b"
@@ -130,7 +130,7 @@
 lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
   by (simp add: box_ne_empty)
 
-subsection%important \<open>Bounds on intervals where they exist\<close>
+subsection \<open>Bounds on intervals where they exist\<close>
 
 definition%important interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
   where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x\<in>s. x\<bullet>i) *\<^sub>R i)"
@@ -192,7 +192,7 @@
       by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
 qed
 
-subsection%important \<open>The notion of a gauge --- simply an open set containing the point\<close>
+subsection \<open>The notion of a gauge --- simply an open set containing the point\<close>
 
 definition%important "gauge \<gamma> \<longleftrightarrow> (\<forall>x. x \<in> \<gamma> x \<and> open (\<gamma> x))"
 
@@ -242,14 +242,14 @@
   "(\<forall>x. \<exists>d :: real. p x \<longrightarrow> 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. p x \<longrightarrow> q d x)"
   by (metis zero_less_one)
 
-subsection%important \<open>Attempt a systematic general set of "offset" results for components\<close>
+subsection \<open>Attempt a systematic general set of "offset" results for components\<close>
 (*FIXME Restructure, the subsection consists only of 1 lemma *)
 lemma gauge_modify:
   assumes "(\<forall>S. open S \<longrightarrow> open {x. f(x) \<in> S})" "gauge d"
   shows "gauge (\<lambda>x. {y. f y \<in> d (f x)})"
   using assms unfolding gauge_def by force
 
-subsection%important \<open>Divisions\<close>
+subsection \<open>Divisions\<close>
 
 definition%important division_of (infixl "division'_of" 40)
 where
@@ -995,7 +995,7 @@
   }
 qed
 
-subsection%important \<open>Tagged (partial) divisions\<close>
+subsection \<open>Tagged (partial) divisions\<close>
 
 definition%important tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40)
   where "s tagged_partial_division_of i \<longleftrightarrow>
@@ -1286,7 +1286,7 @@
 qed
 
 
-subsection%important \<open>Functions closed on boxes: morphisms from boxes to monoids\<close>
+subsection \<open>Functions closed on boxes: morphisms from boxes to monoids\<close>
 
 text \<open>This auxiliary structure is used to sum up over the elements of a division. Main theorem is
   \<open>operative_division\<close>. Instances for the monoid are \<^typ>\<open>'a option\<close>, \<^typ>\<open>real\<close>, and
@@ -1828,7 +1828,7 @@
 qed
 
 
-subsection%important \<open>Special case of additivity we need for the FTC\<close>
+subsection \<open>Special case of additivity we need for the FTC\<close>
 (*fix add explanation here *)
 lemma additive_tagged_division_1:
   fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
@@ -1856,7 +1856,7 @@
 qed
 
 
-subsection%important \<open>Fine-ness of a partition w.r.t. a gauge\<close>
+subsection \<open>Fine-ness of a partition w.r.t. a gauge\<close>
 
 definition%important fine  (infixr "fine" 46)
   where "d fine s \<longleftrightarrow> (\<forall>(x,k) \<in> s. k \<subseteq> d x)"
@@ -1887,7 +1887,7 @@
 lemma fine_subset: "p \<subseteq> q \<Longrightarrow> d fine q \<Longrightarrow> d fine p"
   unfolding fine_def by blast
 
-subsection%important \<open>Some basic combining lemmas\<close>
+subsection \<open>Some basic combining lemmas\<close>
 
 lemma tagged_division_Union_exists:
   assumes "finite I"
@@ -1914,7 +1914,7 @@
   shows "s division_of i \<Longrightarrow> closed i"
   unfolding division_of_def by fastforce
 (* FIXME structure here, do not have one lemma in each subsection *)
-subsection%important \<open>General bisection principle for intervals; might be useful elsewhere\<close>
+subsection \<open>General bisection principle for intervals; might be useful elsewhere\<close>
 (* FIXME  move? *)
 lemma interval_bisection_step:
   fixes type :: "'a::euclidean_space"
@@ -2180,7 +2180,7 @@
 qed
 
 
-subsection%important \<open>Cousin's lemma\<close>
+subsection \<open>Cousin's lemma\<close>
 
 lemma fine_division_exists: (*FIXME rename(?) *)
   fixes a b :: "'a::euclidean_space"
@@ -2226,7 +2226,7 @@
   obtains p where "p tagged_division_of {a .. b}" "g fine p"
   by (metis assms box_real(2) fine_division_exists)
 
-subsection%important \<open>A technical lemma about "refinement" of division\<close>
+subsection \<open>A technical lemma about "refinement" of division\<close>
 
 lemma tagged_division_finer:
   fixes p :: "('a::euclidean_space \<times> ('a::euclidean_space set)) set"
@@ -2301,7 +2301,7 @@
   with ptag that show ?thesis by auto
 qed
 
-subsubsection%important \<open>Covering lemma\<close>
+subsubsection \<open>Covering lemma\<close>
 
 text\<open> Some technical lemmas used in the approximation results that follow. Proof of the covering
   lemma is an obvious multidimensional generalization of Lemma 3, p65 of Swartz's
@@ -2571,7 +2571,7 @@
     qed
 qed
 
-subsection%important \<open>Division filter\<close>
+subsection \<open>Division filter\<close>
 
 text \<open>Divisions over all gauges towards finer divisions.\<close>
 
--- a/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -234,7 +234,7 @@
   qed
 qed
 
-subsection%important\<open>Vitali covering theorem\<close>
+subsection\<open>Vitali covering theorem\<close>
 
 lemma%unimportant Vitali_covering_lemma_cballs:
   fixes a :: "'a \<Rightarrow> 'b::euclidean_space"
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Thu Jan 17 16:37:06 2019 -0500
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Thu Jan 17 16:38:00 2019 -0500
@@ -6,7 +6,7 @@
 imports Uniform_Limit Path_Connected Derivative
 begin
 
-subsection%important \<open>Bernstein polynomials\<close>
+subsection \<open>Bernstein polynomials\<close>
 
 definition%important Bernstein :: "[nat,nat,real] \<Rightarrow> real" where
   "Bernstein n k x \<equiv> of_nat (n choose k) * x ^ k * (1 - x) ^ (n - k)"
@@ -65,7 +65,7 @@
     by auto
 qed
 
-subsection%important \<open>Explicit Bernstein version of the 1D Weierstrass approximation theorem\<close>
+subsection \<open>Explicit Bernstein version of the 1D Weierstrass approximation theorem\<close>
 
 lemma%important Bernstein_Weierstrass:
   fixes f :: "real \<Rightarrow> real"
@@ -167,7 +167,7 @@
 qed
 
 
-subsection%important \<open>General Stone-Weierstrass theorem\<close>
+subsection \<open>General Stone-Weierstrass theorem\<close>
 
 text\<open>Source:
 Bruno Brosowski and Frank Deutsch.
@@ -782,7 +782,7 @@
 qed
 
 
-subsection%important \<open>Polynomial functions\<close>
+subsection \<open>Polynomial functions\<close>
 
 inductive real_polynomial_function :: "('a::real_normed_vector \<Rightarrow> real) \<Rightarrow> bool" where
     linear: "bounded_linear f \<Longrightarrow> real_polynomial_function f"
@@ -983,7 +983,7 @@
     by (simp add: euclidean_representation_sum_fun)
 qed
 
-subsection%important \<open>Stone-Weierstrass theorem for polynomial functions\<close>
+subsection \<open>Stone-Weierstrass theorem for polynomial functions\<close>
 
 text\<open>First, we need to show that they are continous, differentiable and separable.\<close>
 
@@ -1175,7 +1175,7 @@
 qed
 
 
-subsection%important\<open>Polynomial functions as paths\<close>
+subsection\<open>Polynomial functions as paths\<close>
 
 text\<open>One application is to pick a smooth approximation to a path,
 or just pick a smooth path anyway in an open connected set\<close>