subsection is always %important
authorimmler
Thu Jan 17 16:38:00 2019 -0500 (4 months ago)
changeset 696838b3458ca0762
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
     1.1 --- a/src/HOL/Analysis/Arcwise_Connected.thy	Thu Jan 17 16:37:06 2019 -0500
     1.2 +++ b/src/HOL/Analysis/Arcwise_Connected.thy	Thu Jan 17 16:38:00 2019 -0500
     1.3 @@ -8,7 +8,7 @@
     1.4  imports Path_Connected Ordered_Euclidean_Space "HOL-Computational_Algebra.Primes"
     1.5  begin
     1.6  
     1.7 -subsection%important \<open>The Brouwer reduction theorem\<close>
     1.8 +subsection \<open>The Brouwer reduction theorem\<close>
     1.9  
    1.10  theorem Brouwer_reduction_theorem_gen:
    1.11    fixes S :: "'a::euclidean_space set"
    1.12 @@ -108,7 +108,7 @@
    1.13  
    1.14  subsection%unimportant\<open>Arcwise Connections\<close>(*FIX ME this subsection is empty(?) *)
    1.15  
    1.16 -subsection%important\<open>Density of points with dyadic rational coordinates\<close>
    1.17 +subsection\<open>Density of points with dyadic rational coordinates\<close>
    1.18  
    1.19  proposition closure_dyadic_rationals:
    1.20      "closure (\<Union>k. \<Union>f \<in> Basis \<rightarrow> \<int>.
    1.21 @@ -2001,7 +2001,7 @@
    1.22  
    1.23  
    1.24  
    1.25 -subsection%important\<open>Accessibility of frontier points\<close>
    1.26 +subsection\<open>Accessibility of frontier points\<close>
    1.27  
    1.28  lemma dense_accessible_frontier_points:
    1.29    fixes S :: "'a::{complete_space,real_normed_vector} set"
     2.1 --- a/src/HOL/Analysis/Binary_Product_Measure.thy	Thu Jan 17 16:37:06 2019 -0500
     2.2 +++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Thu Jan 17 16:38:00 2019 -0500
     2.3 @@ -14,7 +14,7 @@
     2.4  lemma rev_Pair_vimage_times[simp]: "(\<lambda>x. (x, y)) -` (A \<times> B) = (if y \<in> B then A else {})"
     2.5    by auto
     2.6  
     2.7 -subsection%important "Binary products"
     2.8 +subsection "Binary products"
     2.9  
    2.10  definition%important pair_measure (infixr "\<Otimes>\<^sub>M" 80) where
    2.11    "A \<Otimes>\<^sub>M B = measure_of (space A \<times> space B)
    2.12 @@ -336,7 +336,7 @@
    2.13      by (simp add: ac_simps)
    2.14  qed
    2.15  
    2.16 -subsection%important \<open>Binary products of \<open>\<sigma>\<close>-finite emeasure spaces\<close>
    2.17 +subsection \<open>Binary products of \<open>\<sigma>\<close>-finite emeasure spaces\<close>
    2.18  
    2.19  locale%unimportant pair_sigma_finite = M1?: sigma_finite_measure M1 + M2?: sigma_finite_measure M2
    2.20    for M1 :: "'a measure" and M2 :: "'b measure"
    2.21 @@ -531,7 +531,7 @@
    2.22      done
    2.23  qed
    2.24  
    2.25 -subsection%important "Fubinis theorem"
    2.26 +subsection "Fubinis theorem"
    2.27  
    2.28  lemma measurable_compose_Pair1:
    2.29    "x \<in> space M1 \<Longrightarrow> g \<in> measurable (M1 \<Otimes>\<^sub>M M2) L \<Longrightarrow> (\<lambda>y. g (x, y)) \<in> measurable M2 L"
    2.30 @@ -602,7 +602,7 @@
    2.31    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)"
    2.32    using Fubini[OF f] by simp
    2.33  
    2.34 -subsection%important \<open>Products on counting spaces, densities and distributions\<close>
    2.35 +subsection \<open>Products on counting spaces, densities and distributions\<close>
    2.36  
    2.37  proposition sigma_prod:
    2.38    assumes X_cover: "\<exists>E\<subseteq>A. countable E \<and> X = \<Union>E" and A: "A \<subseteq> Pow X"
    2.39 @@ -1095,7 +1095,7 @@
    2.40  using _ _ assms(1)
    2.41  by(rule measurable_compose_countable'[where f="\<lambda>a b. f (a, snd b)" and g=fst and I=A, simplified])simp_all
    2.42  
    2.43 -subsection%important \<open>Product of Borel spaces\<close>
    2.44 +subsection \<open>Product of Borel spaces\<close>
    2.45  
    2.46  theorem borel_Times:
    2.47    fixes A :: "'a::topological_space set" and B :: "'b::topological_space set"
     3.1 --- a/src/HOL/Analysis/Bochner_Integration.thy	Thu Jan 17 16:37:06 2019 -0500
     3.2 +++ b/src/HOL/Analysis/Bochner_Integration.thy	Thu Jan 17 16:38:00 2019 -0500
     3.3 @@ -2201,7 +2201,7 @@
     3.4    then show ?thesis using \<open>strict_mono r\<close> by auto
     3.5  qed
     3.6  
     3.7 -subsection%important \<open>Restricted measure spaces\<close>
     3.8 +subsection \<open>Restricted measure spaces\<close>
     3.9  
    3.10  lemma integrable_restrict_space:
    3.11    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
    3.12 @@ -2252,7 +2252,7 @@
    3.13    thus ?thesis by simp
    3.14  qed
    3.15  
    3.16 -subsection%important \<open>Measure spaces with an associated density\<close>
    3.17 +subsection \<open>Measure spaces with an associated density\<close>
    3.18  
    3.19  lemma integrable_density:
    3.20    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"
    3.21 @@ -2338,7 +2338,7 @@
    3.22      has_bochner_integral M (\<lambda>x. g x *\<^sub>R f x) x \<Longrightarrow> has_bochner_integral (density M g) f x"
    3.23    by (simp add: has_bochner_integral_iff integrable_density integral_density)
    3.24  
    3.25 -subsection%important \<open>Distributions\<close>
    3.26 +subsection \<open>Distributions\<close>
    3.27  
    3.28  lemma integrable_distr_eq:
    3.29    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
    3.30 @@ -2410,7 +2410,7 @@
    3.31      has_bochner_integral M (\<lambda>x. f (g x)) x \<Longrightarrow> has_bochner_integral (distr M N g) f x"
    3.32    by (simp add: has_bochner_integral_iff integrable_distr_eq integral_distr)
    3.33  
    3.34 -subsection%important \<open>Lebesgue integration on \<^const>\<open>count_space\<close>\<close>
    3.35 +subsection \<open>Lebesgue integration on \<^const>\<open>count_space\<close>\<close>
    3.36  
    3.37  lemma integrable_count_space:
    3.38    fixes f :: "'a \<Rightarrow> 'b::{banach,second_countable_topology}"
    3.39 @@ -2497,7 +2497,7 @@
    3.40    shows "has_bochner_integral (count_space UNIV) f x \<Longrightarrow> f sums x"
    3.41    unfolding has_bochner_integral_iff by (auto intro!: sums_integral_count_space_nat)
    3.42  
    3.43 -subsection%important \<open>Point measure\<close>
    3.44 +subsection \<open>Point measure\<close>
    3.45  
    3.46  lemma lebesgue_integral_point_measure_finite:
    3.47    fixes g :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
    3.48 @@ -2515,7 +2515,7 @@
    3.49    apply (auto simp: AE_count_space integrable_count_space)
    3.50    done
    3.51  
    3.52 -subsection%important \<open>Lebesgue integration on \<^const>\<open>null_measure\<close>\<close>
    3.53 +subsection \<open>Lebesgue integration on \<^const>\<open>null_measure\<close>\<close>
    3.54  
    3.55  lemma has_bochner_integral_null_measure_iff[iff]:
    3.56    "has_bochner_integral (null_measure M) f 0 \<longleftrightarrow> f \<in> borel_measurable M"
    3.57 @@ -2529,7 +2529,7 @@
    3.58    by (cases "integrable (null_measure M) f")
    3.59       (auto simp add: not_integrable_integral_eq has_bochner_integral_integral_eq)
    3.60  
    3.61 -subsection%important \<open>Legacy lemmas for the real-valued Lebesgue integral\<close>
    3.62 +subsection \<open>Legacy lemmas for the real-valued Lebesgue integral\<close>
    3.63  theorem real_lebesgue_integral_def:
    3.64    assumes f[measurable]: "integrable M f"
    3.65    shows "integral\<^sup>L M f = enn2real (\<integral>\<^sup>+x. f x \<partial>M) - enn2real (\<integral>\<^sup>+x. ennreal (- f x) \<partial>M)"
    3.66 @@ -2839,7 +2839,7 @@
    3.67      by (auto simp: _has_bochner_integral_iff)
    3.68  qed
    3.69  
    3.70 -subsection%important \<open>Product measure\<close>
    3.71 +subsection \<open>Product measure\<close>
    3.72  
    3.73  lemma (in sigma_finite_measure) borel_measurable_lebesgue_integrable[measurable (raw)]:
    3.74    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
     4.1 --- a/src/HOL/Analysis/Borel_Space.thy	Thu Jan 17 16:37:06 2019 -0500
     4.2 +++ b/src/HOL/Analysis/Borel_Space.thy	Thu Jan 17 16:38:00 2019 -0500
     4.3 @@ -294,7 +294,7 @@
     4.4    ultimately show ?thesis using that by blast
     4.5  qed
     4.6  
     4.7 -subsection%important \<open>Generic Borel spaces\<close>
     4.8 +subsection \<open>Generic Borel spaces\<close>
     4.9  
    4.10  definition%important (in topological_space) borel :: "'a measure" where
    4.11    "borel = sigma UNIV {S. open S}"
    4.12 @@ -669,7 +669,7 @@
    4.13      unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
    4.14  qed
    4.15  
    4.16 -subsection%important \<open>Borel spaces on order topologies\<close>
    4.17 +subsection \<open>Borel spaces on order topologies\<close>
    4.18  
    4.19  lemma [measurable]:
    4.20    fixes a b :: "'a::linorder_topology"
    4.21 @@ -970,7 +970,7 @@
    4.22    with u show ?thesis by (simp cong: measurable_cong)
    4.23  qed
    4.24  
    4.25 -subsection%important \<open>Borel spaces on topological monoids\<close>
    4.26 +subsection \<open>Borel spaces on topological monoids\<close>
    4.27  
    4.28  lemma borel_measurable_add[measurable (raw)]:
    4.29    fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, topological_monoid_add}"
    4.30 @@ -994,7 +994,7 @@
    4.31    shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M"
    4.32    unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
    4.33  
    4.34 -subsection%important \<open>Borel spaces on Euclidean spaces\<close>
    4.35 +subsection \<open>Borel spaces on Euclidean spaces\<close>
    4.36  
    4.37  lemma borel_measurable_inner[measurable (raw)]:
    4.38    fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_inner}"
    4.39 @@ -1329,7 +1329,7 @@
    4.40      by (subst borel_measurable_iff_halfspace_le) auto
    4.41  qed auto
    4.42  
    4.43 -subsection%important "Borel measurable operators"
    4.44 +subsection "Borel measurable operators"
    4.45  
    4.46  lemma borel_measurable_norm[measurable]: "norm \<in> borel_measurable borel"
    4.47    by (intro borel_measurable_continuous_on1 continuous_intros)
    4.48 @@ -1525,7 +1525,7 @@
    4.49  lemma measurable_of_bool[measurable]: "of_bool \<in> count_space UNIV \<rightarrow>\<^sub>M borel"
    4.50    by simp
    4.51  
    4.52 -subsection%important "Borel space on the extended reals"
    4.53 +subsection "Borel space on the extended reals"
    4.54  
    4.55  lemma borel_measurable_ereal[measurable (raw)]:
    4.56    assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
    4.57 @@ -1686,7 +1686,7 @@
    4.58    shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M"
    4.59    unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
    4.60  
    4.61 -subsection%important "Borel space on the extended non-negative reals"
    4.62 +subsection "Borel space on the extended non-negative reals"
    4.63  
    4.64  text \<open> \<^type>\<open>ennreal\<close> is a topological monoid, so no rules for plus are required, also all order
    4.65    statements are usually done on type classes. \<close>
    4.66 @@ -1760,7 +1760,7 @@
    4.67  
    4.68  hide_const (open) is_borel
    4.69  
    4.70 -subsection%important \<open>LIMSEQ is borel measurable\<close>
    4.71 +subsection \<open>LIMSEQ is borel measurable\<close>
    4.72  
    4.73  lemma borel_measurable_LIMSEQ_real:
    4.74    fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> real"
     5.1 --- a/src/HOL/Analysis/Caratheodory.thy	Thu Jan 17 16:37:06 2019 -0500
     5.2 +++ b/src/HOL/Analysis/Caratheodory.thy	Thu Jan 17 16:38:00 2019 -0500
     5.3 @@ -49,12 +49,12 @@
     5.4      by (simp add: suminf_eq_SUP)
     5.5  qed
     5.6  
     5.7 -subsection%important \<open>Characterizations of Measures\<close>
     5.8 +subsection \<open>Characterizations of Measures\<close>
     5.9  
    5.10  definition%important outer_measure_space where
    5.11    "outer_measure_space M f \<longleftrightarrow> positive M f \<and> increasing M f \<and> countably_subadditive M f"
    5.12  
    5.13 -subsubsection%important \<open>Lambda Systems\<close>
    5.14 +subsubsection \<open>Lambda Systems\<close>
    5.15  
    5.16  definition%important lambda_system :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a set set"
    5.17  where
    5.18 @@ -460,7 +460,7 @@
    5.19  lemma measure_down: "measure_space \<Omega> N \<mu> \<Longrightarrow> sigma_algebra \<Omega> M \<Longrightarrow> M \<subseteq> N \<Longrightarrow> measure_space \<Omega> M \<mu>"
    5.20    by (auto simp add: measure_space_def positive_def countably_additive_def subset_eq)
    5.21  
    5.22 -subsection%important \<open>Caratheodory's theorem\<close>
    5.23 +subsection \<open>Caratheodory's theorem\<close>
    5.24  
    5.25  theorem (in ring_of_sets) caratheodory':
    5.26    assumes posf: "positive M f" and ca: "countably_additive M f"
    5.27 @@ -497,7 +497,7 @@
    5.28    show "\<forall>A\<in>M. f A \<noteq> \<infinity>" using fin by auto
    5.29  qed (rule cont)
    5.30  
    5.31 -subsection%important \<open>Volumes\<close>
    5.32 +subsection \<open>Volumes\<close>
    5.33  
    5.34  definition%important volume :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
    5.35    "volume M f \<longleftrightarrow>
    5.36 @@ -635,7 +635,7 @@
    5.37    qed
    5.38  qed
    5.39  
    5.40 -subsubsection%important \<open>Caratheodory on semirings\<close>
    5.41 +subsubsection \<open>Caratheodory on semirings\<close>
    5.42  
    5.43  theorem (in semiring_of_sets) caratheodory:
    5.44    assumes pos: "positive M \<mu>" and ca: "countably_additive M \<mu>"
     6.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Jan 17 16:37:06 2019 -0500
     6.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Jan 17 16:38:00 2019 -0500
     6.3 @@ -45,7 +45,7 @@
     6.4          "box (vec a) (vec b) = {} \<longleftrightarrow> box a b = {}"
     6.5    by (auto simp: Basis_vec_def mem_box box_eq_empty inner_axis)
     6.6  
     6.7 -subsection%important\<open>Closures and interiors of halfspaces\<close>
     6.8 +subsection\<open>Closures and interiors of halfspaces\<close>
     6.9  
    6.10  lemma%important interior_halfspace_le [simp]:
    6.11    assumes "a \<noteq> 0"
    6.12 @@ -190,7 +190,7 @@
    6.13    by (simp_all add: linear_continuous_at linear_continuous_on)
    6.14  
    6.15  
    6.16 -subsection%important\<open>Bounds on components etc.\ relative to operator norm\<close>
    6.17 +subsection\<open>Bounds on components etc.\ relative to operator norm\<close>
    6.18  
    6.19  lemma%important norm_column_le_onorm:
    6.20    fixes A :: "real^'n^'m"
    6.21 @@ -527,7 +527,7 @@
    6.22      unfolding Collect_all_eq by (simp add: closed_INT)
    6.23  qed
    6.24  
    6.25 -subsection%important "Convex Euclidean Space"
    6.26 +subsection "Convex Euclidean Space"
    6.27  
    6.28  lemma%unimportant Cart_1:"(1::real^'n) = \<Sum>Basis"
    6.29    using const_vector_cart[of 1] by (simp add: one_vec_def)
    6.30 @@ -563,7 +563,7 @@
    6.31  qed
    6.32  
    6.33  
    6.34 -subsection%important "Derivative"
    6.35 +subsection "Derivative"
    6.36  
    6.37  definition%important "jacobian f net = matrix(frechet_derivative f net)"
    6.38  
     7.1 --- a/src/HOL/Analysis/Cartesian_Space.thy	Thu Jan 17 16:37:06 2019 -0500
     7.2 +++ b/src/HOL/Analysis/Cartesian_Space.thy	Thu Jan 17 16:38:00 2019 -0500
     7.3 @@ -501,7 +501,7 @@
     7.4  qed
     7.5  
     7.6  
     7.7 -subsection%important\<open> Rank of a matrix\<close>
     7.8 +subsection\<open> Rank of a matrix\<close>
     7.9  
    7.10  text\<open>Equivalence of row and column rank is taken from George Mackiw's paper, Mathematics Magazine 1995, p. 285.\<close>
    7.11  
    7.12 @@ -942,7 +942,7 @@
    7.13    by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
    7.14  
    7.15  
    7.16 -subsection%important  \<open>Orthogonality of a matrix\<close>
    7.17 +subsection  \<open>Orthogonality of a matrix\<close>
    7.18  
    7.19  definition%important  "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow>
    7.20    transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
    7.21 @@ -1008,7 +1008,7 @@
    7.22  qed
    7.23  
    7.24  
    7.25 -subsection%important \<open> We can find an orthogonal matrix taking any unit vector to any other\<close>
    7.26 +subsection \<open> We can find an orthogonal matrix taking any unit vector to any other\<close>
    7.27  
    7.28  lemma%unimportant  orthogonal_matrix_transpose [simp]:
    7.29       "orthogonal_matrix(transpose A) \<longleftrightarrow> orthogonal_matrix A"
    7.30 @@ -1103,7 +1103,7 @@
    7.31  qed
    7.32  
    7.33  
    7.34 -subsection%important  \<open>Linearity of scaling, and hence isometry, that preserves origin\<close>
    7.35 +subsection  \<open>Linearity of scaling, and hence isometry, that preserves origin\<close>
    7.36  
    7.37  lemma%important  scaling_linear:
    7.38    fixes f :: "'a::real_inner \<Rightarrow> 'a::real_inner"
    7.39 @@ -1138,7 +1138,7 @@
    7.40    by (metis dist_0_norm)
    7.41  
    7.42  
    7.43 -subsection%important  \<open>Can extend an isometry from unit sphere\<close>
    7.44 +subsection  \<open>Can extend an isometry from unit sphere\<close>
    7.45  
    7.46  lemma%important  isometry_sphere_extend:
    7.47    fixes f:: "'a::real_inner \<Rightarrow> 'a"
    7.48 @@ -1178,7 +1178,7 @@
    7.49      by (rule exI[where x= ?g]) (metis thfg thd)
    7.50  qed
    7.51  
    7.52 -subsection%important\<open>Induction on matrix row operations\<close>
    7.53 +subsection\<open>Induction on matrix row operations\<close>
    7.54  
    7.55  lemma%unimportant induct_matrix_row_operations:
    7.56    fixes P :: "real^'n^'n \<Rightarrow> bool"
     8.1 --- a/src/HOL/Analysis/Change_Of_Vars.thy	Thu Jan 17 16:37:06 2019 -0500
     8.2 +++ b/src/HOL/Analysis/Change_Of_Vars.thy	Thu Jan 17 16:38:00 2019 -0500
     8.3 @@ -421,7 +421,7 @@
     8.4      by (simp add: measure_linear_image \<open>linear f\<close> S f)
     8.5  qed
     8.6  
     8.7 -subsection%important\<open>\<open>F_sigma\<close> and \<open>G_delta\<close> sets.\<close>(*FIX ME mv *)
     8.8 +subsection\<open>\<open>F_sigma\<close> and \<open>G_delta\<close> sets.\<close>(*FIX ME mv *)
     8.9  
    8.10  (*https://en.wikipedia.org/wiki/F\<sigma>_set*)
    8.11  inductive%important fsigma :: "'a::topological_space set \<Rightarrow> bool" where
    8.12 @@ -1411,7 +1411,7 @@
    8.13      by (blast intro: order_trans)
    8.14  qed
    8.15  
    8.16 -subsection%important\<open>Borel measurable Jacobian determinant\<close>
    8.17 +subsection\<open>Borel measurable Jacobian determinant\<close>
    8.18  
    8.19  lemma%unimportant lemma_partial_derivatives0:
    8.20    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
    8.21 @@ -2184,7 +2184,7 @@
    8.22  qed
    8.23  
    8.24  
    8.25 -subsection%important\<open>Simplest case of Sard's theorem (we don't need continuity of derivative)\<close>
    8.26 +subsection\<open>Simplest case of Sard's theorem (we don't need continuity of derivative)\<close>
    8.27  
    8.28  lemma%important Sard_lemma00:
    8.29    fixes P :: "'b::euclidean_space set"
    8.30 @@ -2547,7 +2547,7 @@
    8.31  qed
    8.32  
    8.33  
    8.34 -subsection%important\<open>A one-way version of change-of-variables not assuming injectivity. \<close>
    8.35 +subsection\<open>A one-way version of change-of-variables not assuming injectivity. \<close>
    8.36  
    8.37  lemma%important integral_on_image_ubound_weak:
    8.38    fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real"
    8.39 @@ -2960,7 +2960,7 @@
    8.40    using%unimportant integral_on_image_ubound_nonneg [OF assms] by%unimportant simp
    8.41  
    8.42  
    8.43 -subsection%important\<open>Change-of-variables theorem\<close>
    8.44 +subsection\<open>Change-of-variables theorem\<close>
    8.45  
    8.46  text\<open>The classic change-of-variables theorem. We have two versions with quite general hypotheses,
    8.47  the first that the transforming function has a continuous inverse, the second that the base set is
    8.48 @@ -3638,7 +3638,7 @@
    8.49    using%unimportant has_absolute_integral_change_of_variables_1 [OF assms] by%unimportant auto
    8.50  
    8.51  
    8.52 -subsection%important\<open>Change of variables for integrals: special case of linear function\<close>
    8.53 +subsection\<open>Change of variables for integrals: special case of linear function\<close>
    8.54  
    8.55  lemma%unimportant has_absolute_integral_change_of_variables_linear:
    8.56    fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_"
    8.57 @@ -3697,7 +3697,7 @@
    8.58      by blast
    8.59  qed
    8.60  
    8.61 -subsection%important\<open>Change of variable for measure\<close>
    8.62 +subsection\<open>Change of variable for measure\<close>
    8.63  
    8.64  lemma%unimportant has_measure_differentiable_image:
    8.65    fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_"
     9.1 --- a/src/HOL/Analysis/Cross3.thy	Thu Jan 17 16:37:06 2019 -0500
     9.2 +++ b/src/HOL/Analysis/Cross3.thy	Thu Jan 17 16:38:00 2019 -0500
     9.3 @@ -33,7 +33,7 @@
     9.4  
     9.5  unbundle cross3_syntax
     9.6  
     9.7 -subsection%important\<open> Basic lemmas\<close>
     9.8 +subsection\<open> Basic lemmas\<close>
     9.9  
    9.10  lemmas cross3_simps = cross3_def inner_vec_def sum_3 det_3 vec_eq_iff vector_def algebra_simps
    9.11  
    9.12 @@ -168,7 +168,7 @@
    9.13    apply (simp add: cross_mult_left)
    9.14    done
    9.15  
    9.16 -subsection%important   \<open>Preservation by rotation, or other orthogonal transformation up to sign\<close>
    9.17 +subsection   \<open>Preservation by rotation, or other orthogonal transformation up to sign\<close>
    9.18  
    9.19  lemma  cross_matrix_mult: "transpose A *v ((A *v x) \<times> (A *v y)) = det A *\<^sub>R (x \<times> y)"
    9.20    apply (simp add: vec_eq_iff   )
    9.21 @@ -208,7 +208,7 @@
    9.22             \<Longrightarrow> (f x) \<times> (f y) = f(x \<times> y)"
    9.23    by (simp add: cross_orthogonal_transformation orthogonal_transformation)
    9.24  
    9.25 -subsection%important \<open>Continuity\<close>
    9.26 +subsection \<open>Continuity\<close>
    9.27  
    9.28  lemma  continuous_cross: "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. (f x) \<times> (g x))"
    9.29    apply (subst continuous_componentwise)
    10.1 --- a/src/HOL/Analysis/Determinants.thy	Thu Jan 17 16:37:06 2019 -0500
    10.2 +++ b/src/HOL/Analysis/Determinants.thy	Thu Jan 17 16:38:00 2019 -0500
    10.3 @@ -10,7 +10,7 @@
    10.4    "HOL-Library.Permutations"
    10.5  begin
    10.6  
    10.7 -subsection%important  \<open>Trace\<close>
    10.8 +subsection  \<open>Trace\<close>
    10.9  
   10.10  definition%important  trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a"
   10.11    where "trace A = sum (\<lambda>i. ((A$i)$i)) (UNIV::'n set)"
   10.12 @@ -33,7 +33,7 @@
   10.13    apply (simp add: mult.commute)
   10.14    done
   10.15  
   10.16 -subsubsection%important  \<open>Definition of determinant\<close>
   10.17 +subsubsection  \<open>Definition of determinant\<close>
   10.18  
   10.19  definition%important  det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where
   10.20    "det A =
   10.21 @@ -712,7 +712,7 @@
   10.22  qed
   10.23  
   10.24  
   10.25 -subsection%important \<open>Relation to invertibility\<close>
   10.26 +subsection \<open>Relation to invertibility\<close>
   10.27  
   10.28  lemma%important  invertible_det_nz:
   10.29    fixes A::"'a::{field}^'n^'n"
   10.30 @@ -776,7 +776,7 @@
   10.31    using invertible_det_nz [of A]
   10.32    by (auto simp: matrix_left_invertible_injective invertible_left_inverse less_rank_noninjective)
   10.33  
   10.34 -subsubsection%important  \<open>Invertibility of matrices and corresponding linear functions\<close>
   10.35 +subsubsection  \<open>Invertibility of matrices and corresponding linear functions\<close>
   10.36  
   10.37  lemma%important  matrix_left_invertible_gen:
   10.38    fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n"
   10.39 @@ -861,7 +861,7 @@
   10.40        vec.linear_injective_left_inverse vec.linear_surjective_right_inverse)
   10.41  
   10.42  
   10.43 -subsection%important \<open>Cramer's rule\<close>
   10.44 +subsection \<open>Cramer's rule\<close>
   10.45  
   10.46  lemma%important  cramer_lemma_transpose:
   10.47    fixes A:: "'a::{field}^'n^'n"
   10.48 @@ -996,7 +996,7 @@
   10.49    shows "orthogonal_transformation f \<Longrightarrow> \<bar>det (matrix f)\<bar> = 1"
   10.50    using%unimportant det_orthogonal_matrix orthogonal_transformation_matrix by fastforce
   10.51  
   10.52 -subsection%important  \<open>Rotation, reflection, rotoinversion\<close>
   10.53 +subsection  \<open>Rotation, reflection, rotoinversion\<close>
   10.54  
   10.55  definition%important  "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
   10.56  definition%important  "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
    11.1 --- a/src/HOL/Analysis/Elementary_Topology.thy	Thu Jan 17 16:37:06 2019 -0500
    11.2 +++ b/src/HOL/Analysis/Elementary_Topology.thy	Thu Jan 17 16:38:00 2019 -0500
    11.3 @@ -650,7 +650,7 @@
    11.4  qed
    11.5  
    11.6  
    11.7 -subsection%important \<open>Polish spaces\<close>
    11.8 +subsection \<open>Polish spaces\<close>
    11.9  
   11.10  text \<open>Textbooks define Polish spaces as completely metrizable.
   11.11    We assume the topology to be complete for a given metric.\<close>
    12.1 --- a/src/HOL/Analysis/Extended_Real_Limits.thy	Thu Jan 17 16:37:06 2019 -0500
    12.2 +++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Thu Jan 17 16:38:00 2019 -0500
    12.3 @@ -357,7 +357,7 @@
    12.4    done
    12.5  
    12.6  
    12.7 -subsection%important \<open>Extended-Real.thy\<close> (*FIX ME change title *)
    12.8 +subsection \<open>Extended-Real.thy\<close> (*FIX ME change title *)
    12.9  
   12.10  lemma sum_constant_ereal:
   12.11    fixes a::ereal
   12.12 @@ -391,7 +391,7 @@
   12.13  qed
   12.14  
   12.15  
   12.16 -subsubsection%important \<open>Continuity of addition\<close>
   12.17 +subsubsection \<open>Continuity of addition\<close>
   12.18  
   12.19  text \<open>The next few lemmas remove an unnecessary assumption in \<open>tendsto_add_ereal\<close>, culminating
   12.20  in \<open>tendsto_add_ereal_general\<close> which essentially says that the addition
   12.21 @@ -522,7 +522,7 @@
   12.22    then show ?thesis using tendsto_add_ereal_MInf MInf f g by (metis ereal_MInfty_eq_plus)
   12.23  qed
   12.24  
   12.25 -subsubsection%important \<open>Continuity of multiplication\<close>
   12.26 +subsubsection \<open>Continuity of multiplication\<close>
   12.27  
   12.28  text \<open>In the same way as for addition, we prove that the multiplication is continuous on
   12.29  ereal times ereal, except at \<open>(\<infinity>, 0)\<close> and \<open>(-\<infinity>, 0)\<close> and \<open>(0, \<infinity>)\<close> and \<open>(0, -\<infinity>)\<close>,
   12.30 @@ -659,7 +659,7 @@
   12.31  by (cases "c = 0", auto simp add: assms tendsto_mult_ereal)
   12.32  
   12.33  
   12.34 -subsubsection%important \<open>Continuity of division\<close>
   12.35 +subsubsection \<open>Continuity of division\<close>
   12.36  
   12.37  lemma tendsto_inverse_ereal_PInf:
   12.38    fixes u::"_ \<Rightarrow> ereal"
   12.39 @@ -762,7 +762,7 @@
   12.40  qed
   12.41  
   12.42  
   12.43 -subsubsection%important \<open>Further limits\<close>
   12.44 +subsubsection \<open>Further limits\<close>
   12.45  
   12.46  text \<open>The assumptions of @{thm tendsto_diff_ereal} are too strong, we weaken them here.\<close>
   12.47  
   12.48 @@ -958,7 +958,7 @@
   12.49  by (subst uminus_ereal.simps(1)[symmetric], intro tendsto_intros)
   12.50  
   12.51  
   12.52 -subsection%important \<open>Extended-Nonnegative-Real.thy\<close> (*FIX title *)
   12.53 +subsection \<open>Extended-Nonnegative-Real.thy\<close> (*FIX title *)
   12.54  
   12.55  lemma tendsto_diff_ennreal_general [tendsto_intros]:
   12.56    fixes u v::"'a \<Rightarrow> ennreal"
   12.57 @@ -987,7 +987,7 @@
   12.58  qed
   12.59  
   12.60  
   12.61 -subsection%important \<open>monoset\<close> (*FIX ME title *)
   12.62 +subsection \<open>monoset\<close> (*FIX ME title *)
   12.63  
   12.64  definition (in order) mono_set:
   12.65    "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
   12.66 @@ -1759,7 +1759,7 @@
   12.67      by (auto simp: * ereal_diff_positive max.absorb2 liminf_SUP_INF[symmetric] limsup_INF_SUP[symmetric] ereal_liminf_limsup_minus)
   12.68  qed
   12.69  
   12.70 -subsection%important "Relate extended reals and the indicator function"
   12.71 +subsection "Relate extended reals and the indicator function"
   12.72  
   12.73  lemma ereal_indicator_le_0: "(indicator S x::ereal) \<le> 0 \<longleftrightarrow> x \<notin> S"
   12.74    by (auto split: split_indicator simp: one_ereal_def)
    13.1 --- a/src/HOL/Analysis/Fashoda_Theorem.thy	Thu Jan 17 16:37:06 2019 -0500
    13.2 +++ b/src/HOL/Analysis/Fashoda_Theorem.thy	Thu Jan 17 16:38:00 2019 -0500
    13.3 @@ -8,7 +8,7 @@
    13.4  imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
    13.5  begin
    13.6  
    13.7 -subsection%important \<open>Bijections between intervals\<close>
    13.8 +subsection \<open>Bijections between intervals\<close>
    13.9  
   13.10  definition%important interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space"
   13.11    where "interval_bij =
   13.12 @@ -70,7 +70,7 @@
   13.13    using assms by (intro interval_bij_bij) (auto simp: Basis_vec_def inner_axis)
   13.14  
   13.15  
   13.16 -subsection%important \<open>Fashoda meet theorem\<close>
   13.17 +subsection \<open>Fashoda meet theorem\<close>
   13.18  
   13.19  lemma infnorm_2:
   13.20    fixes x :: "real^2"
   13.21 @@ -630,7 +630,7 @@
   13.22  qed
   13.23  
   13.24  
   13.25 -subsection%important \<open>Useful Fashoda corollary pointed out to me by Tom Hales\<close>(*FIXME change title? *)
   13.26 +subsection \<open>Useful Fashoda corollary pointed out to me by Tom Hales\<close>(*FIXME change title? *)
   13.27  
   13.28  corollary fashoda_interlace:
   13.29    fixes a :: "real^2"
    14.1 --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Jan 17 16:37:06 2019 -0500
    14.2 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Jan 17 16:38:00 2019 -0500
    14.3 @@ -68,7 +68,7 @@
    14.4  lemma vec_lambda_eta [simp]: "(\<chi> i. (g$i)) = g"
    14.5    by (simp add: vec_eq_iff)
    14.6  
    14.7 -subsection%important \<open>Cardinality of vectors\<close>
    14.8 +subsection \<open>Cardinality of vectors\<close>
    14.9  
   14.10  instance vec :: (finite, finite) finite
   14.11  proof
   14.12 @@ -292,7 +292,7 @@
   14.13    "scalar_product v w = (\<Sum> i \<in> UNIV. v $ i * w $ i)"
   14.14  
   14.15  
   14.16 -subsection%important \<open>Real vector space\<close>
   14.17 +subsection \<open>Real vector space\<close>
   14.18  
   14.19  instantiation%unimportant vec :: (real_vector, finite) real_vector
   14.20  begin
   14.21 @@ -308,7 +308,7 @@
   14.22  end
   14.23  
   14.24  
   14.25 -subsection%important \<open>Topological space\<close>
   14.26 +subsection \<open>Topological space\<close>
   14.27  
   14.28  instantiation%unimportant vec :: (topological_space, finite) topological_space
   14.29  begin
   14.30 @@ -430,7 +430,7 @@
   14.31  qed
   14.32  
   14.33  
   14.34 -subsection%important \<open>Metric space\<close>
   14.35 +subsection \<open>Metric space\<close>
   14.36  (* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
   14.37  
   14.38  instantiation%unimportant vec :: (metric_space, finite) dist
   14.39 @@ -570,7 +570,7 @@
   14.40  qed
   14.41  
   14.42  
   14.43 -subsection%important \<open>Normed vector space\<close>
   14.44 +subsection \<open>Normed vector space\<close>
   14.45  
   14.46  instantiation%unimportant vec :: (real_normed_vector, finite) real_normed_vector
   14.47  begin
   14.48 @@ -636,7 +636,7 @@
   14.49  instance vec :: (banach, finite) banach ..
   14.50  
   14.51  
   14.52 -subsection%important \<open>Inner product space\<close>
   14.53 +subsection \<open>Inner product space\<close>
   14.54  
   14.55  instantiation%unimportant vec :: (real_inner, finite) real_inner
   14.56  begin
   14.57 @@ -668,7 +668,7 @@
   14.58  end
   14.59  
   14.60  
   14.61 -subsection%important \<open>Euclidean space\<close>
   14.62 +subsection \<open>Euclidean space\<close>
   14.63  
   14.64  text \<open>Vectors pointing along a single axis.\<close>
   14.65  
   14.66 @@ -992,7 +992,7 @@
   14.67    apply (auto )
   14.68    by unfold_locales (vector algebra_simps)+
   14.69  
   14.70 -subsection%important \<open>Matrix operations\<close>
   14.71 +subsection \<open>Matrix operations\<close>
   14.72  
   14.73  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>
   14.74  
   14.75 @@ -1202,7 +1202,7 @@
   14.76    "(A::'a::comm_semiring_1^'n^_) *v x = sum (\<lambda>i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)"
   14.77    by (simp add: matrix_vector_mult_def transpose_def vec_eq_iff mult.commute)
   14.78  
   14.79 -subsection%important\<open>Inverse matrices  (not necessarily square)\<close>
   14.80 +subsection\<open>Inverse matrices  (not necessarily square)\<close>
   14.81  
   14.82  definition%important
   14.83    "invertible(A::'a::semiring_1^'n^'m) \<longleftrightarrow> (\<exists>A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
    15.1 --- a/src/HOL/Analysis/Finite_Product_Measure.thy	Thu Jan 17 16:37:06 2019 -0500
    15.2 +++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Thu Jan 17 16:38:00 2019 -0500
    15.3 @@ -109,9 +109,9 @@
    15.4    "I \<inter> J = {} \<Longrightarrow> merge I J -` Pi\<^sub>E (I \<union> J) E = Pi I E \<times> Pi J E"
    15.5    by (auto simp: restrict_Pi_cancel PiE_def)
    15.6  
    15.7 -subsection%important \<open>Finite product spaces\<close>
    15.8 +subsection \<open>Finite product spaces\<close>
    15.9  
   15.10 -subsubsection%important \<open>Products\<close>
   15.11 +subsubsection \<open>Products\<close>
   15.12  
   15.13  definition%important prod_emb where
   15.14    "prod_emb I M K X = (\<lambda>x. restrict x K) -` X \<inter> (\<Pi>\<^sub>E i\<in>I. space (M i))"
    16.1 --- a/src/HOL/Analysis/Function_Topology.thy	Thu Jan 17 16:37:06 2019 -0500
    16.2 +++ b/src/HOL/Analysis/Function_Topology.thy	Thu Jan 17 16:38:00 2019 -0500
    16.3 @@ -61,9 +61,9 @@
    16.4  I realized afterwards that this theory has a lot in common with \<^file>\<open>~~/src/HOL/Library/Finite_Map.thy\<close>.
    16.5  \<close>
    16.6  
    16.7 -subsection%important \<open>Topology without type classes\<close>
    16.8 +subsection \<open>Topology without type classes\<close>
    16.9  
   16.10 -subsubsection%important \<open>The topology generated by some (open) subsets\<close>
   16.11 +subsubsection \<open>The topology generated by some (open) subsets\<close>
   16.12  
   16.13  text \<open>In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
   16.14  as it follows from \<open>UN\<close> taking for \<open>K\<close> the empty set. However, it is convenient to have,
   16.15 @@ -257,7 +257,7 @@
   16.16    qed
   16.17  qed
   16.18  
   16.19 -subsubsection%important \<open>Continuity\<close>
   16.20 +subsubsection \<open>Continuity\<close>
   16.21  
   16.22  text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
   16.23  of type classes, as defined below.\<close>
   16.24 @@ -336,7 +336,7 @@
   16.25  using assms unfolding continuous_on_topo_def by auto
   16.26  
   16.27  
   16.28 -subsubsection%important \<open>Pullback topology\<close>
   16.29 +subsubsection \<open>Pullback topology\<close>
   16.30  
   16.31  text \<open>Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
   16.32  a special case of this notion, pulling back by the identity. We introduce the general notion as
   16.33 @@ -425,7 +425,7 @@
   16.34  qed
   16.35  
   16.36  
   16.37 -subsection%important \<open>The product topology\<close>
   16.38 +subsection \<open>The product topology\<close>
   16.39  
   16.40  text \<open>We can now define the product topology, as generated by
   16.41  the sets which are products of open sets along finitely many coordinates, and the whole
   16.42 @@ -809,7 +809,7 @@
   16.43  qed
   16.44  
   16.45  
   16.46 -subsubsection%important \<open>Powers of a single topological space as a topological space, using type classes\<close>
   16.47 +subsubsection \<open>Powers of a single topological space as a topological space, using type classes\<close>
   16.48  
   16.49  instantiation "fun" :: (type, topological_space) topological_space
   16.50  begin
   16.51 @@ -885,7 +885,7 @@
   16.52    "continuous_on UNIV f \<longleftrightarrow> (\<forall>i. continuous_on UNIV (\<lambda>x. f x i))"
   16.53  by (auto intro: continuous_on_product_then_coordinatewise)
   16.54  
   16.55 -subsubsection%important \<open>Topological countability for product spaces\<close>
   16.56 +subsubsection \<open>Topological countability for product spaces\<close>
   16.57  
   16.58  text \<open>The next two lemmas are useful to prove first or second countability
   16.59  of product spaces, but they have more to do with countability and could
   16.60 @@ -1116,7 +1116,7 @@
   16.61    using product_topology_countable_basis topological_basis_imp_subbasis by auto
   16.62  
   16.63  
   16.64 -subsection%important \<open>The strong operator topology on continuous linear operators\<close> (* FIX ME mv*)
   16.65 +subsection \<open>The strong operator topology on continuous linear operators\<close> (* FIX ME mv*)
   16.66  
   16.67  text \<open>Let \<open>'a\<close> and \<open>'b\<close> be two normed real vector spaces. Then the space of linear continuous
   16.68  operators from \<open>'a\<close> to \<open>'b\<close> has a canonical norm, and therefore a canonical corresponding topology
   16.69 @@ -1196,7 +1196,7 @@
   16.70      auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
   16.71  
   16.72  
   16.73 -subsection%important \<open>Metrics on product spaces\<close>
   16.74 +subsection \<open>Metrics on product spaces\<close>
   16.75  
   16.76  
   16.77  text \<open>In general, the product topology is not metrizable, unless the index set is countable.
   16.78 @@ -1575,7 +1575,7 @@
   16.79  
   16.80  
   16.81  
   16.82 -subsection%important \<open>Measurability\<close> (*FIX ME move? *)
   16.83 +subsection \<open>Measurability\<close> (*FIX ME move? *)
   16.84  
   16.85  text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
   16.86  generated by open sets in the product, and the product sigma algebra, countably generated by
    17.1 --- a/src/HOL/Analysis/Further_Topology.thy	Thu Jan 17 16:37:06 2019 -0500
    17.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Thu Jan 17 16:38:00 2019 -0500
    17.3 @@ -6,7 +6,7 @@
    17.4    imports Equivalence_Lebesgue_Henstock_Integration Weierstrass_Theorems Polytope Complex_Transcendental
    17.5  begin
    17.6  
    17.7 -subsection%important\<open>A map from a sphere to a higher dimensional sphere is nullhomotopic\<close>
    17.8 +subsection\<open>A map from a sphere to a higher dimensional sphere is nullhomotopic\<close>
    17.9  
   17.10  lemma spheremap_lemma1:
   17.11    fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   17.12 @@ -377,7 +377,7 @@
   17.13  
   17.14  
   17.15  
   17.16 -subsection%important\<open> Some technical lemmas about extending maps from cell complexes\<close>
   17.17 +subsection\<open> Some technical lemmas about extending maps from cell complexes\<close>
   17.18  
   17.19  lemma extending_maps_Union_aux:
   17.20    assumes fin: "finite \<F>"
   17.21 @@ -991,7 +991,7 @@
   17.22  
   17.23  
   17.24  
   17.25 -subsection%important\<open> Special cases and corollaries involving spheres\<close>
   17.26 +subsection\<open> Special cases and corollaries involving spheres\<close>
   17.27  
   17.28  lemma disjnt_Diff1: "X \<subseteq> Y' \<Longrightarrow> disjnt (X - Y) (X' - Y')"
   17.29    by (auto simp: disjnt_def)
   17.30 @@ -1140,7 +1140,7 @@
   17.31      by (rule_tac K="K \<inter> T" and g=g in that) (auto simp: disjnt_iff Diff_Int contg)
   17.32  qed
   17.33  
   17.34 -subsection%important\<open>Extending maps to spheres\<close>
   17.35 +subsection\<open>Extending maps to spheres\<close>
   17.36  
   17.37  (*Up to extend_map_affine_to_sphere_cofinite_gen*)
   17.38  
   17.39 @@ -1892,7 +1892,7 @@
   17.40      done
   17.41  qed
   17.42  
   17.43 -subsection%important\<open> Invariance of domain and corollaries\<close>
   17.44 +subsection\<open> Invariance of domain and corollaries\<close>
   17.45  
   17.46  lemma invariance_of_domain_ball:
   17.47    fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
   17.48 @@ -2742,7 +2742,7 @@
   17.49      using clopen [of S] False  by simp
   17.50  qed
   17.51  
   17.52 -subsection%important\<open>Dimension-based conditions for various homeomorphisms\<close>
   17.53 +subsection\<open>Dimension-based conditions for various homeomorphisms\<close>
   17.54  
   17.55  lemma homeomorphic_subspaces_eq:
   17.56    fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   17.57 @@ -2819,7 +2819,7 @@
   17.58    qed
   17.59  qed
   17.60  
   17.61 -subsection%important\<open>more invariance of domain\<close>(*FIX ME title? *)
   17.62 +subsection\<open>more invariance of domain\<close>(*FIX ME title? *)
   17.63  
   17.64  proposition invariance_of_domain_sphere_affine_set_gen:
   17.65    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   17.66 @@ -3114,7 +3114,7 @@
   17.67  qed
   17.68  
   17.69  
   17.70 -subsection%important\<open>The power, squaring and exponential functions as covering maps\<close>
   17.71 +subsection\<open>The power, squaring and exponential functions as covering maps\<close>
   17.72  
   17.73  proposition covering_space_power_punctured_plane:
   17.74    assumes "0 < n"
   17.75 @@ -3487,7 +3487,7 @@
   17.76  qed
   17.77  
   17.78  
   17.79 -subsection%important\<open>Hence the Borsukian results about mappings into circles\<close>(*FIX ME title *)
   17.80 +subsection\<open>Hence the Borsukian results about mappings into circles\<close>(*FIX ME title *)
   17.81  
   17.82  lemma inessential_eq_continuous_logarithm:
   17.83    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
   17.84 @@ -3637,7 +3637,7 @@
   17.85      by (simp add: *)
   17.86  qed
   17.87  
   17.88 -subsection%important\<open>Upper and lower hemicontinuous functions\<close>
   17.89 +subsection\<open>Upper and lower hemicontinuous functions\<close>
   17.90  
   17.91  text\<open>And relation in the case of preimage map to open and closed maps, and fact that upper and lower
   17.92  hemicontinuity together imply continuity in the sense of the Hausdorff metric (at points where the
   17.93 @@ -3840,7 +3840,7 @@
   17.94  qed
   17.95  
   17.96  
   17.97 -subsection%important\<open>Complex logs exist on various "well-behaved" sets\<close>
   17.98 +subsection\<open>Complex logs exist on various "well-behaved" sets\<close>
   17.99  
  17.100  lemma continuous_logarithm_on_contractible:
  17.101    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
  17.102 @@ -3909,7 +3909,7 @@
  17.103  qed
  17.104  
  17.105  
  17.106 -subsection%important\<open>Another simple case where sphere maps are nullhomotopic\<close>
  17.107 +subsection\<open>Another simple case where sphere maps are nullhomotopic\<close>
  17.108  
  17.109  lemma inessential_spheremap_2_aux:
  17.110    fixes f :: "'a::euclidean_space \<Rightarrow> complex"
  17.111 @@ -3975,7 +3975,7 @@
  17.112  qed
  17.113  
  17.114  
  17.115 -subsection%important\<open>Holomorphic logarithms and square roots\<close>
  17.116 +subsection\<open>Holomorphic logarithms and square roots\<close>
  17.117  
  17.118  lemma contractible_imp_holomorphic_log:
  17.119    assumes holf: "f holomorphic_on S"
  17.120 @@ -4189,7 +4189,7 @@
  17.121  qed
  17.122  
  17.123  
  17.124 -subsection%important\<open>The "Borsukian" property of sets\<close>
  17.125 +subsection\<open>The "Borsukian" property of sets\<close>
  17.126  
  17.127  text\<open>This doesn't have a standard name. Kuratowski uses ``contractible with respect to \<open>[S\<^sup>1]\<close>''
  17.128   while Whyburn uses ``property b''. It's closely related to unicoherence.\<close>
  17.129 @@ -4807,7 +4807,7 @@
  17.130  qed
  17.131  
  17.132  
  17.133 -subsection%important\<open>Unicoherence (closed)\<close>
  17.134 +subsection\<open>Unicoherence (closed)\<close>
  17.135  
  17.136  definition%important unicoherent where
  17.137    "unicoherent U \<equiv>
  17.138 @@ -5051,7 +5051,7 @@
  17.139  qed
  17.140  
  17.141  
  17.142 -subsection%important\<open>Several common variants of unicoherence\<close>
  17.143 +subsection\<open>Several common variants of unicoherence\<close>
  17.144  
  17.145  lemma connected_frontier_simple:
  17.146    fixes S :: "'a :: euclidean_space set"
  17.147 @@ -5104,7 +5104,7 @@
  17.148  qed
  17.149  
  17.150  
  17.151 -subsection%important\<open>Some separation results\<close>
  17.152 +subsection\<open>Some separation results\<close>
  17.153  
  17.154  lemma separation_by_component_closed_pointwise:
  17.155    fixes S :: "'a :: euclidean_space set"
    18.1 --- a/src/HOL/Analysis/Great_Picard.thy	Thu Jan 17 16:37:06 2019 -0500
    18.2 +++ b/src/HOL/Analysis/Great_Picard.thy	Thu Jan 17 16:38:00 2019 -0500
    18.3 @@ -374,7 +374,7 @@
    18.4  qed
    18.5  
    18.6    
    18.7 -subsection%important\<open>The Little Picard Theorem\<close>
    18.8 +subsection\<open>The Little Picard Theorem\<close>
    18.9  
   18.10  proposition Landau_Picard:
   18.11    obtains R
   18.12 @@ -614,7 +614,7 @@
   18.13  qed
   18.14  
   18.15  
   18.16 -subsection%important\<open>The ArzelĂ --Ascoli theorem\<close>
   18.17 +subsection\<open>The ArzelĂ --Ascoli theorem\<close>
   18.18  
   18.19  lemma subsequence_diagonalization_lemma:
   18.20    fixes P :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"
   18.21 @@ -788,7 +788,7 @@
   18.22  
   18.23  
   18.24  
   18.25 -subsubsection%important\<open>Montel's theorem\<close>
   18.26 +subsubsection\<open>Montel's theorem\<close>
   18.27  
   18.28  text\<open>a sequence of holomorphic functions uniformly bounded
   18.29  on compact subsets of an open set S has a subsequence that converges to a
   18.30 @@ -993,7 +993,7 @@
   18.31  
   18.32  
   18.33  
   18.34 -subsection%important\<open>Some simple but useful cases of Hurwitz's theorem\<close>
   18.35 +subsection\<open>Some simple but useful cases of Hurwitz's theorem\<close>
   18.36  
   18.37  proposition Hurwitz_no_zeros:
   18.38    assumes S: "open S" "connected S"
   18.39 @@ -1229,7 +1229,7 @@
   18.40  
   18.41  
   18.42  
   18.43 -subsection%important\<open>The Great Picard theorem\<close>
   18.44 +subsection\<open>The Great Picard theorem\<close>
   18.45  
   18.46  lemma GPicard1:
   18.47    assumes S: "open S" "connected S" and "w \<in> S" "0 < r" "Y \<subseteq> X"
    19.1 --- a/src/HOL/Analysis/Homeomorphism.thy	Thu Jan 17 16:37:06 2019 -0500
    19.2 +++ b/src/HOL/Analysis/Homeomorphism.thy	Thu Jan 17 16:38:00 2019 -0500
    19.3 @@ -36,7 +36,7 @@
    19.4    using assms  apply auto
    19.5    done
    19.6  
    19.7 -subsection%important \<open>Homeomorphism of all convex compact sets with nonempty interior\<close>
    19.8 +subsection \<open>Homeomorphism of all convex compact sets with nonempty interior\<close>
    19.9  
   19.10  proposition ray_to_rel_frontier:
   19.11    fixes a :: "'a::real_inner"
   19.12 @@ -725,7 +725,7 @@
   19.13  by (simp add: rel_frontier_def convex_rel_interior_closure)
   19.14  
   19.15  
   19.16 -subsection%important\<open>Homeomorphisms between punctured spheres and affine sets\<close>
   19.17 +subsection\<open>Homeomorphisms between punctured spheres and affine sets\<close>
   19.18  text\<open>Including the famous stereoscopic projection of the 3-D sphere to the complex plane\<close>
   19.19  
   19.20  text\<open>The special case with centre 0 and radius 1\<close>
   19.21 @@ -1004,7 +1004,7 @@
   19.22      done
   19.23  qed
   19.24  
   19.25 -subsection%important\<open>Locally compact sets in an open set\<close>
   19.26 +subsection\<open>Locally compact sets in an open set\<close>
   19.27  
   19.28  text\<open> Locally compact sets are closed in an open set and are homeomorphic
   19.29    to an absolutely closed set if we have one more dimension to play with.\<close>
   19.30 @@ -1995,7 +1995,7 @@
   19.31      done
   19.32  qed
   19.33  
   19.34 -subsection%important\<open> Lifting of general functions to covering space\<close>
   19.35 +subsection\<open> Lifting of general functions to covering space\<close>
   19.36  
   19.37  proposition covering_space_lift_path_strong:
   19.38    fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
    20.1 --- a/src/HOL/Analysis/Improper_Integral.thy	Thu Jan 17 16:37:06 2019 -0500
    20.2 +++ b/src/HOL/Analysis/Improper_Integral.thy	Thu Jan 17 16:38:00 2019 -0500
    20.3 @@ -4,7 +4,7 @@
    20.4    imports Equivalence_Lebesgue_Henstock_Integration
    20.5  begin
    20.6  
    20.7 -subsection%important \<open>Equiintegrability\<close>
    20.8 +subsection \<open>Equiintegrability\<close>
    20.9  
   20.10  text\<open>The definition here only really makes sense for an elementary set. 
   20.11       We just use compact intervals in applications below.\<close>
   20.12 @@ -226,7 +226,7 @@
   20.13      by auto 
   20.14  qed
   20.15  
   20.16 -subsection%important\<open>Subinterval restrictions for equiintegrable families\<close>
   20.17 +subsection\<open>Subinterval restrictions for equiintegrable families\<close>
   20.18  
   20.19  text\<open>First, some technical lemmas about minimizing a "flat" part of a sum over a division.\<close>
   20.20  
   20.21 @@ -1264,7 +1264,7 @@
   20.22    
   20.23  
   20.24  
   20.25 -subsection%important\<open>Continuity of the indefinite integral\<close>
   20.26 +subsection\<open>Continuity of the indefinite integral\<close>
   20.27  
   20.28  proposition indefinite_integral_continuous:
   20.29    fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
    21.1 --- a/src/HOL/Analysis/Interval_Integral.thy	Thu Jan 17 16:37:06 2019 -0500
    21.2 +++ b/src/HOL/Analysis/Interval_Integral.thy	Thu Jan 17 16:38:00 2019 -0500
    21.3 @@ -37,7 +37,7 @@
    21.4  lemma borel_einterval[measurable]: "einterval a b \<in> sets borel"
    21.5    unfolding einterval_def by measurable
    21.6  
    21.7 -subsection%important \<open>Approximating a (possibly infinite) interval\<close>
    21.8 +subsection \<open>Approximating a (possibly infinite) interval\<close>
    21.9  
   21.10  lemma filterlim_sup1: "(LIM x F. f x :> G1) \<Longrightarrow> (LIM x F. f x :> (sup G1 G2))"
   21.11   unfolding filterlim_def by (auto intro: le_supI1)
   21.12 @@ -151,7 +151,7 @@
   21.13  translations
   21.14    "LBINT x=a..b. f" == "CONST interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
   21.15  
   21.16 -subsection%important\<open>Basic properties of integration over an interval\<close>
   21.17 +subsection\<open>Basic properties of integration over an interval\<close>
   21.18  
   21.19  lemma interval_lebesgue_integral_cong:
   21.20    "a \<le> b \<Longrightarrow> (\<And>x. x \<in> einterval a b \<Longrightarrow> f x = g x) \<Longrightarrow> einterval a b \<in> sets M \<Longrightarrow>
   21.21 @@ -303,7 +303,7 @@
   21.22    (set_integrable M {a<..} f)"
   21.23    unfolding%unimportant interval_lebesgue_integrable_def by auto
   21.24  
   21.25 -subsection%important\<open>Basic properties of integration over an interval wrt lebesgue measure\<close>
   21.26 +subsection\<open>Basic properties of integration over an interval wrt lebesgue measure\<close>
   21.27  
   21.28  lemma interval_integral_zero [simp]:
   21.29    fixes a b :: ereal
   21.30 @@ -476,7 +476,7 @@
   21.31    by (subst interval_lebesgue_integral_le_eq, simp) (rule set_borel_integral_eq_integral)
   21.32  
   21.33  
   21.34 -subsection%important\<open>General limit approximation arguments\<close>
   21.35 +subsection\<open>General limit approximation arguments\<close>
   21.36  
   21.37  proposition interval_integral_Icc_approx_nonneg:
   21.38    fixes a b :: ereal
   21.39 @@ -571,7 +571,7 @@
   21.40      by (simp add: interval_lebesgue_integral_le_eq[symmetric] interval_integral_Icc less_imp_le)
   21.41  qed
   21.42  
   21.43 -subsection%important\<open>A slightly stronger Fundamental Theorem of Calculus\<close>
   21.44 +subsection\<open>A slightly stronger Fundamental Theorem of Calculus\<close>
   21.45  
   21.46  text\<open>Three versions: first, for finite intervals, and then two versions for
   21.47      arbitrary intervals.\<close>
   21.48 @@ -781,7 +781,7 @@
   21.49    qed
   21.50  qed
   21.51  
   21.52 -subsection%important\<open>The substitution theorem\<close>
   21.53 +subsection\<open>The substitution theorem\<close>
   21.54  
   21.55  text\<open>Once again, three versions: first, for finite intervals, and then two versions for
   21.56      arbitrary intervals.\<close>
    22.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Jan 17 16:37:06 2019 -0500
    22.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Jan 17 16:38:00 2019 -0500
    22.3 @@ -297,7 +297,7 @@
    22.4  qed
    22.5  
    22.6  
    22.7 -subsection%important  \<open>Orthogonality of a transformation\<close>
    22.8 +subsection  \<open>Orthogonality of a transformation\<close>
    22.9  
   22.10  definition%important  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
   22.11  
    23.1 --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Thu Jan 17 16:37:06 2019 -0500
    23.2 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Thu Jan 17 16:38:00 2019 -0500
    23.3 @@ -1,4 +1,4 @@
    23.4 -subsection%important \<open>Ordered Euclidean Space\<close>
    23.5 +subsection \<open>Ordered Euclidean Space\<close>
    23.6  
    23.7  theory Ordered_Euclidean_Space
    23.8  imports
    24.1 --- a/src/HOL/Analysis/Poly_Roots.thy	Thu Jan 17 16:37:06 2019 -0500
    24.2 +++ b/src/HOL/Analysis/Poly_Roots.thy	Thu Jan 17 16:38:00 2019 -0500
    24.3 @@ -8,7 +8,7 @@
    24.4  imports Complex_Main
    24.5  begin
    24.6  
    24.7 -subsection%important\<open>Basics about polynomial functions: extremal behaviour and root counts\<close>
    24.8 +subsection\<open>Basics about polynomial functions: extremal behaviour and root counts\<close>
    24.9  
   24.10  lemma%important sub_polyfun:
   24.11    fixes x :: "'a::{comm_ring,monoid_mult}"
    25.1 --- a/src/HOL/Analysis/Polytope.thy	Thu Jan 17 16:37:06 2019 -0500
    25.2 +++ b/src/HOL/Analysis/Polytope.thy	Thu Jan 17 16:38:00 2019 -0500
    25.3 @@ -6,7 +6,7 @@
    25.4  imports Cartesian_Euclidean_Space
    25.5  begin
    25.6  
    25.7 -subsection%important \<open>Faces of a (usually convex) set\<close>
    25.8 +subsection \<open>Faces of a (usually convex) set\<close>
    25.9  
   25.10  definition%important face_of :: "['a::real_vector set, 'a set] \<Rightarrow> bool" (infixr "(face'_of)" 50)
   25.11    where
   25.12 @@ -641,7 +641,7 @@
   25.13           F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<ge> b}"
   25.14  using face_of_halfspace_le [of F "-a" "-b"] by simp
   25.15  
   25.16 -subsection%important\<open>Exposed faces\<close>
   25.17 +subsection\<open>Exposed faces\<close>
   25.18  
   25.19  text\<open>That is, faces that are intersection with supporting hyperplane\<close>
   25.20  
   25.21 @@ -874,7 +874,7 @@
   25.22      unfolding exposed_face_of_def by blast
   25.23  qed
   25.24  
   25.25 -subsection%important\<open>Extreme points of a set: its singleton faces\<close>
   25.26 +subsection\<open>Extreme points of a set: its singleton faces\<close>
   25.27  
   25.28  definition%important extreme_point_of :: "['a::real_vector, 'a set] \<Rightarrow> bool"
   25.29                                 (infixr "(extreme'_point'_of)" 50)
   25.30 @@ -974,7 +974,7 @@
   25.31  apply (auto simp: face_of_singleton hull_same)
   25.32  done
   25.33  
   25.34 -subsection%important\<open>Facets\<close>
   25.35 +subsection\<open>Facets\<close>
   25.36  
   25.37  definition%important facet_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
   25.38                      (infixr "(facet'_of)" 50)
   25.39 @@ -1020,7 +1020,7 @@
   25.40      "F facet_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
   25.41  using facet_of_halfspace_le [of F "-a" "-b"] by simp
   25.42  
   25.43 -subsection%important \<open>Edges: faces of affine dimension 1\<close>
   25.44 +subsection \<open>Edges: faces of affine dimension 1\<close>
   25.45  
   25.46  definition%important edge_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"  (infixr "(edge'_of)" 50)
   25.47    where "e edge_of S \<longleftrightarrow> e face_of S \<and> aff_dim e = 1"
   25.48 @@ -1029,7 +1029,7 @@
   25.49     "S edge_of T \<Longrightarrow> S \<subseteq> T"
   25.50  by (simp add: edge_of_def face_of_imp_subset)
   25.51  
   25.52 -subsection%important\<open>Existence of extreme points\<close>
   25.53 +subsection\<open>Existence of extreme points\<close>
   25.54  
   25.55  lemma%important different_norm_3_collinear_points:
   25.56    fixes a :: "'a::euclidean_space"
   25.57 @@ -1105,7 +1105,7 @@
   25.58      done
   25.59  qed
   25.60  
   25.61 -subsection%important\<open>Krein-Milman, the weaker form\<close>
   25.62 +subsection\<open>Krein-Milman, the weaker form\<close>
   25.63  
   25.64  proposition%important Krein_Milman:
   25.65    fixes S :: "'a::euclidean_space set"
   25.66 @@ -1231,7 +1231,7 @@
   25.67  qed
   25.68  
   25.69  
   25.70 -subsection%important\<open>Applying it to convex hulls of explicitly indicated finite sets\<close>
   25.71 +subsection\<open>Applying it to convex hulls of explicitly indicated finite sets\<close>
   25.72  
   25.73  lemma%important Krein_Milman_polytope:
   25.74    fixes S :: "'a::euclidean_space set"
   25.75 @@ -1599,7 +1599,7 @@
   25.76    finally show "?rhs \<subseteq> ?lhs" .
   25.77  qed
   25.78  
   25.79 -subsection%important\<open>Polytopes\<close>
   25.80 +subsection\<open>Polytopes\<close>
   25.81  
   25.82  definition%important polytope where
   25.83   "polytope S \<equiv> \<exists>v. finite v \<and> S = convex hull v"
   25.84 @@ -1694,7 +1694,7 @@
   25.85  qed
   25.86  
   25.87  
   25.88 -subsection%important\<open>Polyhedra\<close>
   25.89 +subsection\<open>Polyhedra\<close>
   25.90  
   25.91  definition%important polyhedron where
   25.92   "polyhedron S \<equiv>
   25.93 @@ -1787,7 +1787,7 @@
   25.94  by (simp add: affine_imp_polyhedron)
   25.95  
   25.96  
   25.97 -subsection%important\<open>Canonical polyhedron representation making facial structure explicit\<close>
   25.98 +subsection\<open>Canonical polyhedron representation making facial structure explicit\<close>
   25.99  
  25.100  lemma%important polyhedron_Int_affine:
  25.101    fixes S :: "'a :: euclidean_space set"
  25.102 @@ -2689,7 +2689,7 @@
  25.103    by (subst polyhedron_linear_image_eq)
  25.104      (auto simp: bij_uminus intro!: linear_uminus)
  25.105  
  25.106 -subsection%important\<open>Relation between polytopes and polyhedra\<close>
  25.107 +subsection\<open>Relation between polytopes and polyhedra\<close>
  25.108  
  25.109  lemma%important polytope_eq_bounded_polyhedron:
  25.110    fixes S :: "'a :: euclidean_space set"
  25.111 @@ -2755,7 +2755,7 @@
  25.112  by (simp add: polytope_convex_hull polytope_imp_polyhedron)
  25.113  
  25.114  
  25.115 -subsection%important\<open>Relative and absolute frontier of a polytope\<close>
  25.116 +subsection\<open>Relative and absolute frontier of a polytope\<close>
  25.117  
  25.118  lemma rel_boundary_of_convex_hull:
  25.119      fixes S :: "'a::euclidean_space set"
  25.120 @@ -3208,7 +3208,7 @@
  25.121    qed (use C in auto)
  25.122  qed
  25.123  
  25.124 -subsection%important \<open>Simplicial complexes and triangulations\<close>
  25.125 +subsection \<open>Simplicial complexes and triangulations\<close>
  25.126  
  25.127  definition%important simplicial_complex where
  25.128   "simplicial_complex \<C> \<equiv>
  25.129 @@ -3226,7 +3226,7 @@
  25.130                  \<longrightarrow> (T \<inter> T') face_of T \<and> (T \<inter> T') face_of T')"
  25.131  
  25.132  
  25.133 -subsection%important\<open>Refining a cell complex to a simplicial complex\<close>
  25.134 +subsection\<open>Refining a cell complex to a simplicial complex\<close>
  25.135  
  25.136  lemma%important convex_hull_insert_Int_eq:
  25.137    fixes z :: "'a :: euclidean_space"
  25.138 @@ -3894,7 +3894,7 @@
  25.139    qed
  25.140  qed
  25.141  
  25.142 -subsection%important\<open>Some results on cell division with full-dimensional cells only\<close>
  25.143 +subsection\<open>Some results on cell division with full-dimensional cells only\<close>
  25.144  
  25.145  lemma%important convex_Union_fulldim_cells:
  25.146    assumes "finite \<S>" and clo: "\<And>C. C \<in> \<S> \<Longrightarrow> closed C" and con: "\<And>C. C \<in> \<S> \<Longrightarrow> convex C"
    26.1 --- a/src/HOL/Analysis/Radon_Nikodym.thy	Thu Jan 17 16:37:06 2019 -0500
    26.2 +++ b/src/HOL/Analysis/Radon_Nikodym.thy	Thu Jan 17 16:38:00 2019 -0500
    26.3 @@ -163,7 +163,7 @@
    26.4    qed measurable
    26.5  qed
    26.6  
    26.7 -subsection%important "Absolutely continuous"
    26.8 +subsection "Absolutely continuous"
    26.9  
   26.10  definition%important absolutely_continuous :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
   26.11    "absolutely_continuous M N \<longleftrightarrow> null_sets M \<subseteq> null_sets N"
   26.12 @@ -198,7 +198,7 @@
   26.13    qed
   26.14  qed
   26.15  
   26.16 -subsection%important "Existence of the Radon-Nikodym derivative"
   26.17 +subsection "Existence of the Radon-Nikodym derivative"
   26.18  
   26.19  lemma%important
   26.20   (in finite_measure) Radon_Nikodym_finite_measure:
   26.21 @@ -607,7 +607,7 @@
   26.22      by (auto intro!: bexI[of _ "\<lambda>x. h x * f x"] simp: density_density_eq)
   26.23  qed
   26.24  
   26.25 -subsection%important \<open>Uniqueness of densities\<close>
   26.26 +subsection \<open>Uniqueness of densities\<close>
   26.27  
   26.28  lemma%important finite_density_unique:
   26.29    assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   26.30 @@ -887,7 +887,7 @@
   26.31    by (subst sigma_finite_iff_density_finite')
   26.32       (auto simp: max_def intro!: measurable_If)
   26.33  
   26.34 -subsection%important \<open>Radon-Nikodym derivative\<close>
   26.35 +subsection \<open>Radon-Nikodym derivative\<close>
   26.36  
   26.37  definition%important RN_deriv :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a \<Rightarrow> ennreal" where
   26.38    "RN_deriv M N =
    27.1 --- a/src/HOL/Analysis/Tagged_Division.thy	Thu Jan 17 16:37:06 2019 -0500
    27.2 +++ b/src/HOL/Analysis/Tagged_Division.thy	Thu Jan 17 16:38:00 2019 -0500
    27.3 @@ -55,7 +55,7 @@
    27.4      by (simp add: field_simps)
    27.5  qed
    27.6  
    27.7 -subsection%important \<open>Some useful lemmas about intervals\<close>
    27.8 +subsection \<open>Some useful lemmas about intervals\<close>
    27.9  
   27.10  lemma interior_subset_union_intervals:
   27.11    assumes "i = cbox a b"
   27.12 @@ -130,7 +130,7 @@
   27.13  lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
   27.14    by (simp add: box_ne_empty)
   27.15  
   27.16 -subsection%important \<open>Bounds on intervals where they exist\<close>
   27.17 +subsection \<open>Bounds on intervals where they exist\<close>
   27.18  
   27.19  definition%important interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
   27.20    where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x\<in>s. x\<bullet>i) *\<^sub>R i)"
   27.21 @@ -192,7 +192,7 @@
   27.22        by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
   27.23  qed
   27.24  
   27.25 -subsection%important \<open>The notion of a gauge --- simply an open set containing the point\<close>
   27.26 +subsection \<open>The notion of a gauge --- simply an open set containing the point\<close>
   27.27  
   27.28  definition%important "gauge \<gamma> \<longleftrightarrow> (\<forall>x. x \<in> \<gamma> x \<and> open (\<gamma> x))"
   27.29  
   27.30 @@ -242,14 +242,14 @@
   27.31    "(\<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)"
   27.32    by (metis zero_less_one)
   27.33  
   27.34 -subsection%important \<open>Attempt a systematic general set of "offset" results for components\<close>
   27.35 +subsection \<open>Attempt a systematic general set of "offset" results for components\<close>
   27.36  (*FIXME Restructure, the subsection consists only of 1 lemma *)
   27.37  lemma gauge_modify:
   27.38    assumes "(\<forall>S. open S \<longrightarrow> open {x. f(x) \<in> S})" "gauge d"
   27.39    shows "gauge (\<lambda>x. {y. f y \<in> d (f x)})"
   27.40    using assms unfolding gauge_def by force
   27.41  
   27.42 -subsection%important \<open>Divisions\<close>
   27.43 +subsection \<open>Divisions\<close>
   27.44  
   27.45  definition%important division_of (infixl "division'_of" 40)
   27.46  where
   27.47 @@ -995,7 +995,7 @@
   27.48    }
   27.49  qed
   27.50  
   27.51 -subsection%important \<open>Tagged (partial) divisions\<close>
   27.52 +subsection \<open>Tagged (partial) divisions\<close>
   27.53  
   27.54  definition%important tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40)
   27.55    where "s tagged_partial_division_of i \<longleftrightarrow>
   27.56 @@ -1286,7 +1286,7 @@
   27.57  qed
   27.58  
   27.59  
   27.60 -subsection%important \<open>Functions closed on boxes: morphisms from boxes to monoids\<close>
   27.61 +subsection \<open>Functions closed on boxes: morphisms from boxes to monoids\<close>
   27.62  
   27.63  text \<open>This auxiliary structure is used to sum up over the elements of a division. Main theorem is
   27.64    \<open>operative_division\<close>. Instances for the monoid are \<^typ>\<open>'a option\<close>, \<^typ>\<open>real\<close>, and
   27.65 @@ -1828,7 +1828,7 @@
   27.66  qed
   27.67  
   27.68  
   27.69 -subsection%important \<open>Special case of additivity we need for the FTC\<close>
   27.70 +subsection \<open>Special case of additivity we need for the FTC\<close>
   27.71  (*fix add explanation here *)
   27.72  lemma additive_tagged_division_1:
   27.73    fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
   27.74 @@ -1856,7 +1856,7 @@
   27.75  qed
   27.76  
   27.77  
   27.78 -subsection%important \<open>Fine-ness of a partition w.r.t. a gauge\<close>
   27.79 +subsection \<open>Fine-ness of a partition w.r.t. a gauge\<close>
   27.80  
   27.81  definition%important fine  (infixr "fine" 46)
   27.82    where "d fine s \<longleftrightarrow> (\<forall>(x,k) \<in> s. k \<subseteq> d x)"
   27.83 @@ -1887,7 +1887,7 @@
   27.84  lemma fine_subset: "p \<subseteq> q \<Longrightarrow> d fine q \<Longrightarrow> d fine p"
   27.85    unfolding fine_def by blast
   27.86  
   27.87 -subsection%important \<open>Some basic combining lemmas\<close>
   27.88 +subsection \<open>Some basic combining lemmas\<close>
   27.89  
   27.90  lemma tagged_division_Union_exists:
   27.91    assumes "finite I"
   27.92 @@ -1914,7 +1914,7 @@
   27.93    shows "s division_of i \<Longrightarrow> closed i"
   27.94    unfolding division_of_def by fastforce
   27.95  (* FIXME structure here, do not have one lemma in each subsection *)
   27.96 -subsection%important \<open>General bisection principle for intervals; might be useful elsewhere\<close>
   27.97 +subsection \<open>General bisection principle for intervals; might be useful elsewhere\<close>
   27.98  (* FIXME  move? *)
   27.99  lemma interval_bisection_step:
  27.100    fixes type :: "'a::euclidean_space"
  27.101 @@ -2180,7 +2180,7 @@
  27.102  qed
  27.103  
  27.104  
  27.105 -subsection%important \<open>Cousin's lemma\<close>
  27.106 +subsection \<open>Cousin's lemma\<close>
  27.107  
  27.108  lemma fine_division_exists: (*FIXME rename(?) *)
  27.109    fixes a b :: "'a::euclidean_space"
  27.110 @@ -2226,7 +2226,7 @@
  27.111    obtains p where "p tagged_division_of {a .. b}" "g fine p"
  27.112    by (metis assms box_real(2) fine_division_exists)
  27.113  
  27.114 -subsection%important \<open>A technical lemma about "refinement" of division\<close>
  27.115 +subsection \<open>A technical lemma about "refinement" of division\<close>
  27.116  
  27.117  lemma tagged_division_finer:
  27.118    fixes p :: "('a::euclidean_space \<times> ('a::euclidean_space set)) set"
  27.119 @@ -2301,7 +2301,7 @@
  27.120    with ptag that show ?thesis by auto
  27.121  qed
  27.122  
  27.123 -subsubsection%important \<open>Covering lemma\<close>
  27.124 +subsubsection \<open>Covering lemma\<close>
  27.125  
  27.126  text\<open> Some technical lemmas used in the approximation results that follow. Proof of the covering
  27.127    lemma is an obvious multidimensional generalization of Lemma 3, p65 of Swartz's
  27.128 @@ -2571,7 +2571,7 @@
  27.129      qed
  27.130  qed
  27.131  
  27.132 -subsection%important \<open>Division filter\<close>
  27.133 +subsection \<open>Division filter\<close>
  27.134  
  27.135  text \<open>Divisions over all gauges towards finer divisions.\<close>
  27.136  
    28.1 --- a/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Thu Jan 17 16:37:06 2019 -0500
    28.2 +++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Thu Jan 17 16:38:00 2019 -0500
    28.3 @@ -234,7 +234,7 @@
    28.4    qed
    28.5  qed
    28.6  
    28.7 -subsection%important\<open>Vitali covering theorem\<close>
    28.8 +subsection\<open>Vitali covering theorem\<close>
    28.9  
   28.10  lemma%unimportant Vitali_covering_lemma_cballs:
   28.11    fixes a :: "'a \<Rightarrow> 'b::euclidean_space"
    29.1 --- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Thu Jan 17 16:37:06 2019 -0500
    29.2 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Thu Jan 17 16:38:00 2019 -0500
    29.3 @@ -6,7 +6,7 @@
    29.4  imports Uniform_Limit Path_Connected Derivative
    29.5  begin
    29.6  
    29.7 -subsection%important \<open>Bernstein polynomials\<close>
    29.8 +subsection \<open>Bernstein polynomials\<close>
    29.9  
   29.10  definition%important Bernstein :: "[nat,nat,real] \<Rightarrow> real" where
   29.11    "Bernstein n k x \<equiv> of_nat (n choose k) * x ^ k * (1 - x) ^ (n - k)"
   29.12 @@ -65,7 +65,7 @@
   29.13      by auto
   29.14  qed
   29.15  
   29.16 -subsection%important \<open>Explicit Bernstein version of the 1D Weierstrass approximation theorem\<close>
   29.17 +subsection \<open>Explicit Bernstein version of the 1D Weierstrass approximation theorem\<close>
   29.18  
   29.19  lemma%important Bernstein_Weierstrass:
   29.20    fixes f :: "real \<Rightarrow> real"
   29.21 @@ -167,7 +167,7 @@
   29.22  qed
   29.23  
   29.24  
   29.25 -subsection%important \<open>General Stone-Weierstrass theorem\<close>
   29.26 +subsection \<open>General Stone-Weierstrass theorem\<close>
   29.27  
   29.28  text\<open>Source:
   29.29  Bruno Brosowski and Frank Deutsch.
   29.30 @@ -782,7 +782,7 @@
   29.31  qed
   29.32  
   29.33  
   29.34 -subsection%important \<open>Polynomial functions\<close>
   29.35 +subsection \<open>Polynomial functions\<close>
   29.36  
   29.37  inductive real_polynomial_function :: "('a::real_normed_vector \<Rightarrow> real) \<Rightarrow> bool" where
   29.38      linear: "bounded_linear f \<Longrightarrow> real_polynomial_function f"
   29.39 @@ -983,7 +983,7 @@
   29.40      by (simp add: euclidean_representation_sum_fun)
   29.41  qed
   29.42  
   29.43 -subsection%important \<open>Stone-Weierstrass theorem for polynomial functions\<close>
   29.44 +subsection \<open>Stone-Weierstrass theorem for polynomial functions\<close>
   29.45  
   29.46  text\<open>First, we need to show that they are continous, differentiable and separable.\<close>
   29.47  
   29.48 @@ -1175,7 +1175,7 @@
   29.49  qed
   29.50  
   29.51  
   29.52 -subsection%important\<open>Polynomial functions as paths\<close>
   29.53 +subsection\<open>Polynomial functions as paths\<close>
   29.54  
   29.55  text\<open>One application is to pick a smooth approximation to a path,
   29.56  or just pick a smooth path anyway in an open connected set\<close>