# HG changeset patch
# User immler
# Date 1523028890 -7200
# Node ID 0acdcd8f4ba11b6cc2ae8f6d8653d93515a4d146
# Parent  9c31678d21392e0c9a553095fb4899a587db9865
a first shot at tagging for HOL-Analysis manual

diff -r 9c31678d2139 -r 0acdcd8f4ba1 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Fri Apr 06 17:34:50 2018 +0200
@@ -468,6 +468,12 @@
 
 text\<open>Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"}\<close>
 
+definition map_matrix::"('a \<Rightarrow> 'b) \<Rightarrow> (('a, 'i::finite)vec, 'j::finite) vec \<Rightarrow> (('b, 'i)vec, 'j) vec" where
+  "map_matrix f x = (\<chi> i j. f (x $ i $ j))"
+
+lemma nth_map_matrix[simp]: "map_matrix f x $ i $ j = f (x $ i $ j)"
+  by (simp add: map_matrix_def)
+
 definition matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m"
     (infixl "**" 70)
   where "m ** m' == (\<chi> i j. sum (\<lambda>k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"
diff -r 9c31678d2139 -r 0acdcd8f4ba1 src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Connected.thy	Fri Apr 06 17:34:50 2018 +0200
@@ -8,7 +8,7 @@
 imports Topology_Euclidean_Space
 begin
 
-subsection \<open>More properties of closed balls, spheres, etc.\<close>
+subsection%unimportant \<open>More properties of closed balls, spheres, etc.\<close>
 
 lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
   apply (simp add: interior_def, safe)
@@ -345,7 +345,7 @@
   shows "closed (sphere a r)"
 by (simp add: compact_imp_closed)
 
-subsection \<open>Connectedness\<close>
+subsection%unimportant \<open>Connectedness\<close>
 
 lemma connected_local:
  "connected S \<longleftrightarrow>
@@ -410,7 +410,7 @@
 
 subsection \<open>Connected components, considered as a connectedness relation or a set\<close>
 
-definition "connected_component s x y \<equiv> \<exists>t. connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t"
+definition%important "connected_component s x y \<equiv> \<exists>t. connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t"
 
 abbreviation "connected_component_set s x \<equiv> Collect (connected_component s x)"
 
@@ -610,7 +610,7 @@
 
 subsection \<open>The set of connected components of a set\<close>
 
-definition components:: "'a::topological_space set \<Rightarrow> 'a set set"
+definition%important components:: "'a::topological_space set \<Rightarrow> 'a set set"
   where "components s \<equiv> connected_component_set s ` s"
 
 lemma components_iff: "s \<in> components u \<longleftrightarrow> (\<exists>x. x \<in> u \<and> s = connected_component_set u x)"
@@ -776,12 +776,12 @@
 
 subsection \<open>Intersecting chains of compact sets and the Baire property\<close>
 
-proposition bounded_closed_chain:
+proposition%important bounded_closed_chain:
   fixes \<F> :: "'a::heine_borel set set"
   assumes "B \<in> \<F>" "bounded B" and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> closed S" and "{} \<notin> \<F>"
       and chain: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
     shows "\<Inter>\<F> \<noteq> {}"
-proof -
+proof%unimportant -
   have "B \<inter> \<Inter>\<F> \<noteq> {}"
   proof (rule compact_imp_fip)
     show "compact B" "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
@@ -824,12 +824,12 @@
   then show ?thesis by blast
 qed
 
-corollary compact_chain:
+corollary%important compact_chain:
   fixes \<F> :: "'a::heine_borel set set"
   assumes "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" "{} \<notin> \<F>"
           "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
     shows "\<Inter> \<F> \<noteq> {}"
-proof (cases "\<F> = {}")
+proof%unimportant (cases "\<F> = {}")
   case True
   then show ?thesis by auto
 next
@@ -852,12 +852,12 @@
 qed
 
 text\<open>The Baire property of dense sets\<close>
-theorem Baire:
+theorem%important Baire:
   fixes S::"'a::{real_normed_vector,heine_borel} set"
   assumes "closed S" "countable \<G>"
       and ope: "\<And>T. T \<in> \<G> \<Longrightarrow> openin (subtopology euclidean S) T \<and> S \<subseteq> closure T"
  shows "S \<subseteq> closure(\<Inter>\<G>)"
-proof (cases "\<G> = {}")
+proof%unimportant (cases "\<G> = {}")
   case True
   then show ?thesis
     using closure_subset by auto
@@ -961,7 +961,7 @@
   qed
 qed
 
-subsection\<open>Some theorems on sups and infs using the notion "bounded".\<close>
+subsection%unimportant \<open>Some theorems on sups and infs using the notion "bounded".\<close>
 
 lemma bounded_real: "bounded (S::real set) \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. \<bar>x\<bar> \<le> a)"
   by (simp add: bounded_iff)
@@ -1139,7 +1139,7 @@
 qed
 
 
-subsection\<open>Relations among convergence and absolute convergence for power series.\<close>
+subsection%unimportant\<open>Relations among convergence and absolute convergence for power series.\<close>
 
 lemma summable_imp_bounded:
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
@@ -1166,7 +1166,7 @@
     done
 qed
 
-subsection \<open>Bounded closed nest property (proof does not use Heine-Borel)\<close>
+subsection%unimportant \<open>Bounded closed nest property (proof does not use Heine-Borel)\<close>
 
 lemma bounded_closed_nest:
   fixes s :: "nat \<Rightarrow> ('a::heine_borel) set"
@@ -1286,7 +1286,7 @@
 
 subsection \<open>Infimum Distance\<close>
 
-definition "infdist x A = (if A = {} then 0 else INF a:A. dist x a)"
+definition%important "infdist x A = (if A = {} then 0 else INF a:A. dist x a)"
 
 lemma bdd_below_image_dist[intro, simp]: "bdd_below (dist x ` A)"
   by (auto intro!: zero_le_dist)
@@ -1515,7 +1515,7 @@
     by (simp add: compact_eq_bounded_closed)
 qed
 
-subsection \<open>Equality of continuous functions on closure and related results.\<close>
+subsection%unimportant \<open>Equality of continuous functions on closure and related results.\<close>
 
 lemma continuous_closedin_preimage_constant:
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
@@ -1618,7 +1618,7 @@
   qed
 qed
 
-subsection \<open>A function constant on a set\<close>
+subsection%unimportant \<open>A function constant on a set\<close>
 
 definition constant_on  (infixl "(constant'_on)" 50)
   where "f constant_on A \<equiv> \<exists>y. \<forall>x\<in>A. f x = y"
@@ -1639,7 +1639,7 @@
 using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def
 by metis
 
-subsection\<open>Relating linear images to open/closed/interior/closure\<close>
+subsection%unimportant\<open>Relating linear images to open/closed/interior/closure\<close>
 
 proposition open_surjective_linear_image:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
@@ -1786,7 +1786,7 @@
   qed
 qed
 
-subsection\<open> Theorems relating continuity and uniform continuity to closures\<close>
+subsection%unimportant\<open> Theorems relating continuity and uniform continuity to closures\<close>
 
 lemma continuous_on_closure:
    "continuous_on (closure S) f \<longleftrightarrow>
@@ -2047,7 +2047,7 @@
   shows "bounded(f ` S)"
   by (metis (no_types, lifting) assms bounded_closure_image compact_closure compact_continuous_image compact_eq_bounded_closed image_cong uniformly_continuous_imp_continuous uniformly_continuous_on_extension_on_closure)
 
-subsection \<open>Making a continuous function avoid some value in a neighbourhood.\<close>
+subsection%unimportant \<open>Making a continuous function avoid some value in a neighbourhood.\<close>
 
 lemma continuous_within_avoid:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
@@ -2097,7 +2097,7 @@
   using continuous_at_avoid[of x f a] assms(4)
   by auto
 
-subsection\<open>Quotient maps\<close>
+subsection%unimportant\<open>Quotient maps\<close>
 
 lemma quotient_map_imp_continuous_open:
   assumes T: "f ` S \<subseteq> T"
@@ -2447,15 +2447,15 @@
   ultimately show ?thesis using that by blast
 qed
 
-corollary compact_uniformly_continuous:
+corollary%important compact_uniformly_continuous:
   fixes f :: "'a :: metric_space \<Rightarrow> 'b :: metric_space"
   assumes f: "continuous_on S f" and S: "compact S"
   shows "uniformly_continuous_on S f"
-  using f
+  using%unimportant f
     unfolding continuous_on_iff uniformly_continuous_on_def
     by (force intro: compact_uniformly_equicontinuous [OF S, of "{f}"])
 
-subsection \<open>Topological stuff about the set of Reals\<close>
+subsection%unimportant \<open>Topological stuff about the set of Reals\<close>
 
 lemma open_real:
   fixes s :: "real set"
@@ -2492,7 +2492,7 @@
   unfolding continuous_on_iff dist_norm by simp
 
 
-subsection \<open>Cartesian products\<close>
+subsection%unimportant \<open>Cartesian products\<close>
 
 lemma bounded_Times:
   assumes "bounded s" "bounded t"
@@ -2668,7 +2668,7 @@
 
 subsection \<open>The diameter of a set.\<close>
 
-definition diameter :: "'a::metric_space set \<Rightarrow> real" where
+definition%important diameter :: "'a::metric_space set \<Rightarrow> real" where
   "diameter S = (if S = {} then 0 else SUP (x,y):S\<times>S. dist x y)"
 
 lemma diameter_empty [simp]: "diameter{} = 0"
@@ -2933,11 +2933,11 @@
 
 subsection \<open>Separation between points and sets\<close>
 
-lemma separate_point_closed:
+lemma%important separate_point_closed:
   fixes s :: "'a::heine_borel set"
   assumes "closed s" and "a \<notin> s"
   shows "\<exists>d>0. \<forall>x\<in>s. d \<le> dist a x"
-proof (cases "s = {}")
+proof%unimportant (cases "s = {}")
   case True
   then show ?thesis by(auto intro!: exI[where x=1])
 next
@@ -2948,12 +2948,12 @@
     by blast
 qed
 
-lemma separate_compact_closed:
+lemma%important separate_compact_closed:
   fixes s t :: "'a::heine_borel set"
   assumes "compact s"
     and t: "closed t" "s \<inter> t = {}"
   shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
-proof cases
+proof%unimportant cases
   assume "s \<noteq> {} \<and> t \<noteq> {}"
   then have "s \<noteq> {}" "t \<noteq> {}" by auto
   let ?inf = "\<lambda>x. infdist x t"
@@ -2968,27 +2968,27 @@
   ultimately show ?thesis by auto
 qed (auto intro!: exI[of _ 1])
 
-lemma separate_closed_compact:
+lemma%important separate_closed_compact:
   fixes s t :: "'a::heine_borel set"
   assumes "closed s"
     and "compact t"
     and "s \<inter> t = {}"
   shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
-proof -
+proof%unimportant -
   have *: "t \<inter> s = {}"
     using assms(3) by auto
   show ?thesis
     using separate_compact_closed[OF assms(2,1) *] by (force simp: dist_commute)
 qed
 
-lemma compact_in_open_separated:
+lemma%important compact_in_open_separated:
   fixes A::"'a::heine_borel set"
   assumes "A \<noteq> {}"
   assumes "compact A"
   assumes "open B"
   assumes "A \<subseteq> B"
   obtains e where "e > 0" "{x. infdist x A \<le> e} \<subseteq> B"
-proof atomize_elim
+proof%unimportant atomize_elim
   have "closed (- B)" "compact A" "- B \<inter> A = {}"
     using assms by (auto simp: open_Diff compact_eq_bounded_closed)
   from separate_closed_compact[OF this]
@@ -3014,7 +3014,7 @@
 qed
 
 
-subsection \<open>Compact sets and the closure operation.\<close>
+subsection%unimportant \<open>Compact sets and the closure operation.\<close>
 
 lemma closed_scaling:
   fixes S :: "'a::real_normed_vector set"
@@ -3165,7 +3165,7 @@
 done
 
 
-subsection \<open>Closure of halfspaces and hyperplanes\<close>
+subsection%unimportant \<open>Closure of halfspaces and hyperplanes\<close>
 
 lemma continuous_on_closed_Collect_le:
   fixes f g :: "'a::t2_space \<Rightarrow> real"
@@ -3492,7 +3492,7 @@
 
 subsection \<open>Homeomorphisms\<close>
 
-definition "homeomorphism s t f g \<longleftrightarrow>
+definition%important "homeomorphism s t f g \<longleftrightarrow>
   (\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and>
   (\<forall>y\<in>t. (f(g y) = y)) \<and> (g ` t = s) \<and> continuous_on t g"
 
@@ -3812,7 +3812,7 @@
 using assms unfolding homeomorphic_def homeomorphism_def by (metis connected_continuous_image)
 
 
-subsection\<open>Inverse function property for open/closed maps\<close>
+subsection%unimportant\<open>Inverse function property for open/closed maps\<close>
 
 lemma continuous_on_inverse_open_map:
   assumes contf: "continuous_on S f"
@@ -3963,12 +3963,12 @@
     unfolding complete_def by auto
 qed
 
-lemma injective_imp_isometric:
+lemma%important injective_imp_isometric:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes s: "closed s" "subspace s"
     and f: "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0"
   shows "\<exists>e>0. \<forall>x\<in>s. norm (f x) \<ge> e * norm x"
-proof (cases "s \<subseteq> {0::'a}")
+proof%unimportant (cases "s \<subseteq> {0::'a}")
   case True
   have "norm x \<le> norm (f x)" if "x \<in> s" for x
   proof -
@@ -4036,11 +4036,11 @@
   ultimately show ?thesis by auto
 qed
 
-lemma closed_injective_image_subspace:
+lemma%important closed_injective_image_subspace:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "subspace s" "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0" "closed s"
   shows "closed(f ` s)"
-proof -
+proof%unimportant -
   obtain e where "e > 0" and e: "\<forall>x\<in>s. e * norm x \<le> norm (f x)"
     using injective_imp_isometric[OF assms(4,1,2,3)] by auto
   show ?thesis
@@ -4049,7 +4049,7 @@
 qed
 
 
-subsection \<open>Some properties of a canonical subspace\<close>
+subsection%unimportant \<open>Some properties of a canonical subspace\<close>
 
 lemma subspace_substandard: "subspace {x::'a::euclidean_space. (\<forall>i\<in>Basis. P i \<longrightarrow> x\<bullet>i = 0)}"
   by (auto simp: subspace_def inner_add_left)
@@ -4157,7 +4157,7 @@
 qed
 
 
-subsection \<open>Affine transformations of intervals\<close>
+subsection%unimportant \<open>Affine transformations of intervals\<close>
 
 lemma real_affinity_le: "0 < m \<Longrightarrow> m * x + c \<le> y \<longleftrightarrow> x \<le> inverse m * y + - (c / m)"
   for m :: "'a::linordered_field"
@@ -4186,13 +4186,13 @@
 
 subsection \<open>Banach fixed point theorem (not really topological ...)\<close>
 
-theorem banach_fix:
+theorem%important banach_fix:
   assumes s: "complete s" "s \<noteq> {}"
     and c: "0 \<le> c" "c < 1"
     and f: "f ` s \<subseteq> s"
     and lipschitz: "\<forall>x\<in>s. \<forall>y\<in>s. dist (f x) (f y) \<le> c * dist x y"
   shows "\<exists>!x\<in>s. f x = x"
-proof -
+proof%unimportant -
   from c have "1 - c > 0" by simp
 
   from s(2) obtain z0 where z0: "z0 \<in> s" by blast
@@ -4342,13 +4342,13 @@
 
 subsection \<open>Edelstein fixed point theorem\<close>
 
-theorem edelstein_fix:
+theorem%important edelstein_fix:
   fixes s :: "'a::metric_space set"
   assumes s: "compact s" "s \<noteq> {}"
     and gs: "(g ` s) \<subseteq> s"
     and dist: "\<forall>x\<in>s. \<forall>y\<in>s. x \<noteq> y \<longrightarrow> dist (g x) (g y) < dist x y"
   shows "\<exists>!x\<in>s. g x = x"
-proof -
+proof%unimportant -
   let ?D = "(\<lambda>x. (x, x)) ` s"
   have D: "compact ?D" "?D \<noteq> {}"
     by (rule compact_continuous_image)
@@ -4697,10 +4697,10 @@
     done
 qed
 
-proposition separable:
+proposition%important separable:
   fixes S :: "'a:: euclidean_space set"
   obtains T where "countable T" "T \<subseteq> S" "S \<subseteq> closure T"
-proof -
+proof%unimportant -
   obtain \<B> :: "'a:: euclidean_space set set"
     where "countable \<B>"
       and "{} \<notin> \<B>"
@@ -4743,11 +4743,11 @@
   qed
 qed
 
-proposition Lindelof:
+proposition%important Lindelof:
   fixes \<F> :: "'a::euclidean_space set set"
   assumes \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> open S"
   obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
-proof -
+proof%unimportant -
   obtain \<B> :: "'a set set"
     where "countable \<B>" "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
       and \<B>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
@@ -5049,11 +5049,11 @@
 qed
 
 
-proposition component_diff_connected:
+proposition%important component_diff_connected:
   fixes S :: "'a::metric_space set"
   assumes "connected S" "connected U" "S \<subseteq> U" and C: "C \<in> components (U - S)"
   shows "connected(U - C)"
-  using \<open>connected S\<close> unfolding connected_closedin_eq not_ex de_Morgan_conj
+  using%unimportant \<open>connected S\<close> unfolding connected_closedin_eq not_ex de_Morgan_conj
 proof clarify
   fix H3 H4 
   assume clo3: "closedin (subtopology euclidean (U - C)) H3" 
@@ -5093,7 +5093,7 @@
     by auto
 qed
 
-subsection\<open> Finite intersection property\<close>
+subsection%unimportant\<open> Finite intersection property\<close>
 
 text\<open>Also developed in HOL's toplogical spaces theory, but the Heine-Borel type class isn't available there.\<close>
 
@@ -5149,7 +5149,7 @@
 by (simp add: closed_limpt islimpt_insert sequence_unique_limpt)
 
 
-subsection\<open>Componentwise limits and continuity\<close>
+subsection%unimportant\<open>Componentwise limits and continuity\<close>
 
 text\<open>But is the premise really necessary? Need to generalise @{thm euclidean_dist_l2}\<close>
 lemma Euclidean_dist_upper: "i \<in> Basis \<Longrightarrow> dist (x \<bullet> i) (y \<bullet> i) \<le> dist x y"
@@ -5179,11 +5179,11 @@
     by (metis (no_types, lifting) \<open>0 < e\<close> \<open>open S\<close> half_gt_zero_iff mem_Collect_eq mem_ball open_contains_ball_eq subsetI)
 qed
 
-proposition tendsto_componentwise_iff:
+proposition%important tendsto_componentwise_iff:
   fixes f :: "_ \<Rightarrow> 'b::euclidean_space"
   shows "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>i \<in> Basis. ((\<lambda>x. (f x \<bullet> i)) \<longlongrightarrow> (l \<bullet> i)) F)"
          (is "?lhs = ?rhs")
-proof
+proof%unimportant
   assume ?lhs
   then show ?rhs
     unfolding tendsto_def
@@ -5267,9 +5267,9 @@
     by (force simp: bounded_linear_def bounded_linear_axioms_def \<open>linear f'\<close>)
 qed
 
-subsection\<open>Pasting functions together\<close>
-
-subsubsection\<open>on open sets\<close>
+subsection%unimportant\<open>Pasting functions together\<close>
+
+subsubsection%unimportant\<open>on open sets\<close>
 
 lemma pasting_lemma:
   fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
@@ -5311,7 +5311,7 @@
     by (metis (no_types, lifting) IntD2 IntI f someI_ex)
 qed
 
-subsubsection\<open>Likewise on closed sets, with a finiteness assumption\<close>
+subsubsection%unimportant\<open>Likewise on closed sets, with a finiteness assumption\<close>
 
 lemma pasting_lemma_closed:
   fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
@@ -5436,7 +5436,7 @@
 qed
 
 
-subsection\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
+subsection%unimportant\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
 
 text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
 
@@ -5595,7 +5595,7 @@
 
 
 
-subsection \<open>Continuous Extension\<close>
+subsection%unimportant \<open>Continuous Extension\<close>
 
 definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   "clamp a b x = (if (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)
diff -r 9c31678d2139 -r 0acdcd8f4ba1 src/HOL/Analysis/Continuous_Extension.thy
--- a/src/HOL/Analysis/Continuous_Extension.thy	Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Continuous_Extension.thy	Fri Apr 06 17:34:50 2018 +0200
@@ -13,7 +13,7 @@
 text\<open>A difference from HOL Light: all summations over infinite sets equal zero,
    so the "support" must be made explicit in the summation below!\<close>
 
-proposition subordinate_partition_of_unity:
+proposition%important subordinate_partition_of_unity:
   fixes S :: "'a :: euclidean_space set"
   assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
       and fin: "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. U \<inter> V \<noteq> {}}"
@@ -22,7 +22,7 @@
       and "\<And>x U. \<lbrakk>U \<in> \<C>; x \<in> S; x \<notin> U\<rbrakk> \<Longrightarrow> F U x = 0"
       and "\<And>x. x \<in> S \<Longrightarrow> supp_sum (\<lambda>W. F W x) \<C> = 1"
       and "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. F U x \<noteq> 0}"
-proof (cases "\<exists>W. W \<in> \<C> \<and> S \<subseteq> W")
+proof%unimportant (cases "\<exists>W. W \<in> \<C> \<and> S \<subseteq> W")
   case True
     then obtain W where "W \<in> \<C>" "S \<subseteq> W" by metis
     then show ?thesis
@@ -283,7 +283,7 @@
           "\<And>x. f x = b \<longleftrightarrow> x \<in> T"
 using assms by (auto intro: Urysohn_local_strong [of UNIV S T])
 
-proposition Urysohn:
+proposition%important Urysohn:
   assumes US: "closed S"
       and UT: "closed T"
       and "S \<inter> T = {}"
@@ -292,22 +292,22 @@
           "\<And>x. f x \<in> closed_segment a b"
           "\<And>x. x \<in> S \<Longrightarrow> f x = a"
           "\<And>x. x \<in> T \<Longrightarrow> f x = b"
-using assms by (auto intro: Urysohn_local [of UNIV S T a b])
+using%unimportant assms by (auto intro: Urysohn_local [of UNIV S T a b])
 
 
 subsection\<open> The Dugundji extension theorem, and Tietze variants as corollaries.\<close>
 
-text\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367.
+text%important\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367.
 http://projecteuclid.org/euclid.pjm/1103052106\<close>
 
-theorem Dugundji:
+theorem%important Dugundji:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
   assumes "convex C" "C \<noteq> {}"
       and cloin: "closedin (subtopology euclidean U) S"
       and contf: "continuous_on S f" and "f ` S \<subseteq> C"
   obtains g where "continuous_on U g" "g ` U \<subseteq> C"
                   "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-proof (cases "S = {}")
+proof%unimportant (cases "S = {}")
   case True then show thesis
     apply (rule_tac g="\<lambda>x. SOME y. y \<in> C" in that)
       apply (rule continuous_intros)
@@ -475,7 +475,7 @@
 qed
 
 
-corollary Tietze:
+corollary%important Tietze:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
   assumes "continuous_on S f"
       and "closedin (subtopology euclidean U) S"
@@ -483,7 +483,7 @@
       and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> B"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
                   "\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> B"
-using assms
+using%unimportant assms
 by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f])
 
 corollary Tietze_closed_interval:
diff -r 9c31678d2139 -r 0acdcd8f4ba1 src/HOL/Analysis/Continuum_Not_Denumerable.thy
--- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Fri Apr 06 17:34:50 2018 +0200
@@ -11,7 +11,7 @@
   "HOL-Library.Countable_Set"
 begin
 
-subsection \<open>Abstract\<close>
+subsection%unimportant \<open>Abstract\<close>
 
 text \<open>
   The following document presents a proof that the Continuum is uncountable.
@@ -33,8 +33,8 @@
   Nested Interval Property.
 \<close>
 
-theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
-proof
+theorem%important real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
+proof%unimportant
   assume "\<exists>f::nat \<Rightarrow> real. surj f"
   then obtain f :: "nat \<Rightarrow> real" where "surj f" ..
 
diff -r 9c31678d2139 -r 0acdcd8f4ba1 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Fri Apr 06 17:34:50 2018 +0200
@@ -177,7 +177,7 @@
 
 subsection \<open>Convexity\<close>
 
-definition convex :: "'a::real_vector set \<Rightarrow> bool"
+definition%important convex :: "'a::real_vector set \<Rightarrow> bool"
   where "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
 
 lemma convexI:
@@ -350,7 +350,7 @@
   by (simp add: convex_def scaleR_conv_of_real)
 
 
-subsection \<open>Explicit expressions for convexity in terms of arbitrary sums\<close>
+subsection%unimportant \<open>Explicit expressions for convexity in terms of arbitrary sums\<close>
 
 lemma convex_sum:
   fixes C :: "'a::real_vector set"
@@ -503,7 +503,7 @@
 
 subsection \<open>Functions that are convex on a set\<close>
 
-definition convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
+definition%important convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
   where "convex_on s f \<longleftrightarrow>
     (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y)"
 
@@ -624,7 +624,7 @@
 qed
 
 
-subsection \<open>Arithmetic operations on sets preserve convexity\<close>
+subsection%unimportant \<open>Arithmetic operations on sets preserve convexity\<close>
 
 lemma convex_linear_image:
   assumes "linear f"
@@ -1087,7 +1087,7 @@
 qed
 
 
-subsection \<open>Convexity of real functions\<close>
+subsection%unimportant \<open>Convexity of real functions\<close>
 
 lemma convex_on_realI:
   assumes "connected A"
@@ -1406,7 +1406,7 @@
 
 subsection \<open>Affine set and affine hull\<close>
 
-definition affine :: "'a::real_vector set \<Rightarrow> bool"
+definition%important affine :: "'a::real_vector set \<Rightarrow> bool"
   where "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
 
 lemma affine_alt: "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \<in> s)"
@@ -1444,7 +1444,7 @@
   by (simp add: affine_def algebra_simps) (metis distrib_right mult.left_neutral)
 
 
-subsubsection \<open>Some explicit formulations (from Lars Schewe)\<close>
+subsubsection%unimportant \<open>Some explicit formulations (from Lars Schewe)\<close>
 
 lemma affine:
   fixes V::"'a::real_vector set"
@@ -1668,7 +1668,7 @@
 qed
 
 
-subsubsection \<open>Stepping theorems and hence small special cases\<close>
+subsubsection%unimportant \<open>Stepping theorems and hence small special cases\<close>
 
 lemma affine_hull_empty[simp]: "affine hull {} = {}"
   by (rule hull_unique) auto
@@ -1806,7 +1806,7 @@
   by (metis add_uminus_conv_diff mem_affine_3_minus real_vector.scale_minus_left)
 
 
-subsubsection \<open>Some relations between affine hull and subspaces\<close>
+subsubsection%unimportant \<open>Some relations between affine hull and subspaces\<close>
 
 lemma affine_hull_insert_subset_span:
   "affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}"
@@ -1867,7 +1867,7 @@
   using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto
 
 
-subsubsection \<open>Parallel affine sets\<close>
+subsubsection%unimportant \<open>Parallel affine sets\<close>
 
 definition affine_parallel :: "'a::real_vector set \<Rightarrow> 'a::real_vector set \<Rightarrow> bool"
   where "affine_parallel S T \<longleftrightarrow> (\<exists>a. T = (\<lambda>x. a + x) ` S)"
@@ -1974,7 +1974,7 @@
   unfolding subspace_def affine_def by auto
 
 
-subsubsection \<open>Subspace parallel to an affine set\<close>
+subsubsection%unimportant \<open>Subspace parallel to an affine set\<close>
 
 lemma subspace_affine: "subspace S \<longleftrightarrow> affine S \<and> 0 \<in> S"
 proof -
@@ -2100,7 +2100,7 @@
 
 subsection \<open>Cones\<close>
 
-definition cone :: "'a::real_vector set \<Rightarrow> bool"
+definition%important cone :: "'a::real_vector set \<Rightarrow> bool"
   where "cone s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>c\<ge>0. c *\<^sub>R x \<in> s)"
 
 lemma cone_empty[intro, simp]: "cone {}"
@@ -2214,9 +2214,9 @@
   shows "c *\<^sub>R x \<in> cone hull S"
   by (metis assms cone_cone_hull hull_inc mem_cone)
 
-lemma cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
+lemma%important cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
   (is "?lhs = ?rhs")
-proof -
+proof%unimportant -
   {
     fix x
     assume "x \<in> ?rhs"
@@ -2282,7 +2282,7 @@
 
 subsection \<open>Affine dependence and consequential theorems (from Lars Schewe)\<close>
 
-definition affine_dependent :: "'a::real_vector set \<Rightarrow> bool"
+definition%important affine_dependent :: "'a::real_vector set \<Rightarrow> bool"
   where "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> affine hull (s - {x}))"
 
 lemma affine_dependent_subset:
@@ -2299,11 +2299,11 @@
    "~ affine_dependent s \<Longrightarrow> ~ affine_dependent(s - t)"
 by (meson Diff_subset affine_dependent_subset)
 
-lemma affine_dependent_explicit:
+lemma%important affine_dependent_explicit:
   "affine_dependent p \<longleftrightarrow>
     (\<exists>s u. finite s \<and> s \<subseteq> p \<and> sum u s = 0 \<and>
       (\<exists>v\<in>s. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) s = 0)"
-  unfolding affine_dependent_def affine_hull_explicit mem_Collect_eq
+  unfolding%unimportant affine_dependent_def affine_hull_explicit mem_Collect_eq
   apply rule
   apply (erule bexE, erule exE, erule exE)
   apply (erule conjE)+
@@ -2365,7 +2365,7 @@
 qed
 
 
-subsection \<open>Connectedness of convex sets\<close>
+subsection%unimportant \<open>Connectedness of convex sets\<close>
 
 lemma connectedD:
   "connected S \<Longrightarrow> open A \<Longrightarrow> open B \<Longrightarrow> S \<subseteq> A \<union> B \<Longrightarrow> A \<inter> B \<inter> S = {} \<Longrightarrow> A \<inter> S = {} \<or> B \<inter> S = {}"
@@ -2558,7 +2558,7 @@
   by auto
 
 
-subsubsection \<open>Convex hull is "preserved" by a linear function\<close>
+subsubsection%unimportant \<open>Convex hull is "preserved" by a linear function\<close>
 
 lemma convex_hull_linear_image:
   assumes f: "linear f"
@@ -2616,7 +2616,7 @@
 qed
 
 
-subsubsection \<open>Stepping theorems for convex hulls of finite sets\<close>
+subsubsection%unimportant \<open>Stepping theorems for convex hulls of finite sets\<close>
 
 lemma convex_hull_empty[simp]: "convex hull {} = {}"
   by (rule hull_unique) auto
@@ -2742,16 +2742,16 @@
   using diff_eq_eq apply fastforce
   by (metis add.group_left_neutral add_le_imp_le_diff diff_add_cancel)
 
-subsubsection \<open>Explicit expression for convex hull\<close>
-
-lemma convex_hull_indexed:
+subsubsection%unimportant \<open>Explicit expression for convex hull\<close>
+
+lemma%important convex_hull_indexed:
   fixes s :: "'a::real_vector set"
   shows "convex hull s =
     {y. \<exists>k u x.
       (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>
       (sum u {1..k} = 1) \<and> (sum (\<lambda>i. u i *\<^sub>R x i) {1..k} = y)}"
   (is "?xyz = ?hull")
-  apply (rule hull_unique)
+  apply%unimportant (rule hull_unique)
   apply rule
   defer
   apply (rule convexI)
@@ -2887,7 +2887,7 @@
 qed
 
 
-subsubsection \<open>Another formulation from Lars Schewe\<close>
+subsubsection%unimportant \<open>Another formulation from Lars Schewe\<close>
 
 lemma convex_hull_explicit:
   fixes p :: "'a::real_vector set"
@@ -2991,7 +2991,7 @@
 qed
 
 
-subsubsection \<open>A stepping theorem for that expansion\<close>
+subsubsection%unimportant \<open>A stepping theorem for that expansion\<close>
 
 lemma convex_hull_finite_step:
   fixes s :: "'a::real_vector set"
@@ -3061,7 +3061,7 @@
 qed
 
 
-subsubsection \<open>Hence some special cases\<close>
+subsubsection%unimportant \<open>Hence some special cases\<close>
 
 lemma convex_hull_2:
   "convex hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b | u v. 0 \<le> u \<and> 0 \<le> v \<and> u + v = 1}"
@@ -3141,7 +3141,7 @@
 qed
 
 
-subsection \<open>Relations among closure notions and corresponding hulls\<close>
+subsection%unimportant \<open>Relations among closure notions and corresponding hulls\<close>
 
 lemma affine_imp_convex: "affine s \<Longrightarrow> convex s"
   unfolding affine_def convex_def by auto
@@ -3306,7 +3306,7 @@
 qed
 
 
-subsection \<open>Some Properties of Affine Dependent Sets\<close>
+subsection%unimportant \<open>Some Properties of Affine Dependent Sets\<close>
 
 lemma affine_independent_0 [simp]: "\<not> affine_dependent {}"
   by (simp add: affine_dependent_def)
@@ -3546,7 +3546,7 @@
 
 subsection \<open>Affine Dimension of a Set\<close>
 
-definition aff_dim :: "('a::euclidean_space) set \<Rightarrow> int"
+definition%important aff_dim :: "('a::euclidean_space) set \<Rightarrow> int"
   where "aff_dim V =
   (SOME d :: int.
     \<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = d + 1)"
@@ -4417,11 +4417,11 @@
     by (auto simp add: convex_hull_explicit)
 qed
 
-theorem caratheodory:
+theorem%important caratheodory:
   "convex hull p =
     {x::'a::euclidean_space. \<exists>s. finite s \<and> s \<subseteq> p \<and>
       card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s}"
-proof safe
+proof%unimportant safe
   fix x
   assume "x \<in> convex hull p"
   then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1"
@@ -4444,7 +4444,7 @@
 
 subsection \<open>Relative interior of a set\<close>
 
-definition "rel_interior S =
+definition%important "rel_interior S =
   {x. \<exists>T. openin (subtopology euclidean (affine hull S)) T \<and> x \<in> T \<and> T \<subseteq> S}"
 
 lemma rel_interior_mono:
@@ -4769,7 +4769,7 @@
 
 subsubsection \<open>Relative open sets\<close>
 
-definition "rel_open S \<longleftrightarrow> rel_interior S = S"
+definition%important "rel_open S \<longleftrightarrow> rel_interior S = S"
 
 lemma rel_open: "rel_open S \<longleftrightarrow> openin (subtopology euclidean (affine hull S)) S"
   unfolding rel_open_def rel_interior_def
@@ -4970,7 +4970,7 @@
 qed
 
 
-subsubsection\<open>Relative interior preserves under linear transformations\<close>
+subsubsection%unimportant\<open>Relative interior preserves under linear transformations\<close>
 
 lemma rel_interior_translation_aux:
   fixes a :: "'n::euclidean_space"
@@ -5134,7 +5134,7 @@
   by auto
 
 
-subsection\<open>Some Properties of subset of standard basis\<close>
+subsection%unimportant\<open>Some Properties of subset of standard basis\<close>
 
 lemma affine_hull_substd_basis:
   assumes "d \<subseteq> Basis"
@@ -5151,7 +5151,7 @@
   by (metis Int_absorb1 Int_absorb2 convex_hull_subset_affine_hull hull_hull hull_mono hull_subset)
 
 
-subsection \<open>Openness and compactness are preserved by convex hull operation.\<close>
+subsection%unimportant \<open>Openness and compactness are preserved by convex hull operation.\<close>
 
 lemma open_convex_hull[intro]:
   fixes s :: "'a::real_normed_vector set"
@@ -5422,7 +5422,7 @@
 qed
 
 
-subsection \<open>Extremal points of a simplex are some vertices.\<close>
+subsection%unimportant \<open>Extremal points of a simplex are some vertices.\<close>
 
 lemma dist_increases_online:
   fixes a b d :: "'a::real_inner"
@@ -5623,7 +5623,7 @@
 
 subsection \<open>Closest point of a convex set is unique, with a continuous projection.\<close>
 
-definition closest_point :: "'a::{real_inner,heine_borel} set \<Rightarrow> 'a \<Rightarrow> 'a"
+definition%important closest_point :: "'a::{real_inner,heine_borel} set \<Rightarrow> 'a \<Rightarrow> 'a"
   where "closest_point s a = (SOME x. x \<in> s \<and> (\<forall>y\<in>s. dist a x \<le> dist a y))"
 
 lemma closest_point_exists:
@@ -5811,7 +5811,7 @@
 qed
 
 
-subsubsection \<open>Various point-to-set separating/supporting hyperplane theorems.\<close>
+subsubsection%unimportant \<open>Various point-to-set separating/supporting hyperplane theorems.\<close>
 
 lemma supporting_hyperplane_closed_point:
   fixes z :: "'a::{real_inner,heine_borel}"
@@ -5933,7 +5933,7 @@
 qed
 
 
-subsubsection \<open>Now set-to-set for closed/compact sets\<close>
+subsubsection%unimportant \<open>Now set-to-set for closed/compact sets\<close>
 
 lemma separating_hyperplane_closed_compact:
   fixes S :: "'a::euclidean_space set"
@@ -6024,7 +6024,7 @@
 qed
 
 
-subsubsection \<open>General case without assuming closure and getting non-strict separation\<close>
+subsubsection%unimportant \<open>General case without assuming closure and getting non-strict separation\<close>
 
 lemma separating_hyperplane_set_0:
   assumes "convex s" "(0::'a::euclidean_space) \<notin> s"
@@ -6082,7 +6082,7 @@
 qed
 
 
-subsection \<open>More convexity generalities\<close>
+subsection%unimportant \<open>More convexity generalities\<close>
 
 lemma convex_closure [intro,simp]:
   fixes s :: "'a::real_normed_vector set"
@@ -6132,7 +6132,7 @@
   using hull_subset[of s convex] convex_hull_empty by auto
 
 
-subsection \<open>Moving and scaling convex hulls.\<close>
+subsection%unimportant \<open>Moving and scaling convex hulls.\<close>
 
 lemma convex_hull_set_plus:
   "convex hull (s + t) = convex hull s + convex hull t"
@@ -6159,7 +6159,7 @@
   by(simp only: image_image[symmetric] convex_hull_scaling convex_hull_translation)
 
 
-subsection \<open>Convexity of cone hulls\<close>
+subsection%unimportant \<open>Convexity of cone hulls\<close>
 
 lemma convex_cone_hull:
   assumes "convex S"
@@ -6227,7 +6227,7 @@
     using \<open>S \<noteq> {}\<close> cone_iff[of "convex hull S"] by auto
 qed
 
-subsection \<open>Convex set as intersection of halfspaces\<close>
+subsection%unimportant \<open>Convex set as intersection of halfspaces\<close>
 
 lemma convex_halfspace_intersection:
   fixes s :: "('a::euclidean_space) set"
@@ -6381,10 +6381,10 @@
     done
 qed
 
-lemma radon:
+theorem%important radon:
   assumes "affine_dependent c"
   obtains m p where "m \<subseteq> c" "p \<subseteq> c" "m \<inter> p = {}" "(convex hull m) \<inter> (convex hull p) \<noteq> {}"
-proof -
+proof%unimportant -
   from assms[unfolded affine_dependent_explicit]
   obtain s u where
       "finite s" "s \<subseteq> c" "sum u s = 0" "\<exists>v\<in>s. u v \<noteq> 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0"
@@ -6503,12 +6503,12 @@
   qed auto
 qed
 
-lemma helly:
+theorem%important helly:
   fixes f :: "'a::euclidean_space set set"
   assumes "card f \<ge> DIM('a) + 1" "\<forall>s\<in>f. convex s"
     and "\<forall>t\<subseteq>f. card t = DIM('a) + 1 \<longrightarrow> \<Inter>t \<noteq> {}"
   shows "\<Inter>f \<noteq> {}"
-  apply (rule helly_induct)
+  apply%unimportant (rule helly_induct)
   using assms
   apply auto
   done
@@ -6516,7 +6516,7 @@
 
 subsection \<open>Epigraphs of convex functions\<close>
 
-definition "epigraph s (f :: _ \<Rightarrow> real) = {xy. fst xy \<in> s \<and> f (fst xy) \<le> snd xy}"
+definition%important "epigraph s (f :: _ \<Rightarrow> real) = {xy. fst xy \<in> s \<and> f (fst xy) \<le> snd xy}"
 
 lemma mem_epigraph: "(x, y) \<in> epigraph s f \<longleftrightarrow> x \<in> s \<and> f x \<le> y"
   unfolding epigraph_def by auto
@@ -6545,7 +6545,7 @@
   by (simp add: convex_epigraph)
 
 
-subsubsection \<open>Use this to derive general bound property of convex function\<close>
+subsubsection%unimportant \<open>Use this to derive general bound property of convex function\<close>
 
 lemma convex_on:
   assumes "convex s"
@@ -6572,7 +6572,7 @@
   done
 
 
-subsection \<open>Convexity of general and special intervals\<close>
+subsection%unimportant \<open>Convexity of general and special intervals\<close>
 
 lemma is_interval_convex:
   fixes s :: "'a::euclidean_space set"
@@ -6657,7 +6657,7 @@
      "\<lbrakk>connected S; aff_dim S \<noteq> 0; a \<in> S\<rbrakk> \<Longrightarrow> a islimpt S"
   using aff_dim_sing connected_imp_perfect by blast
 
-subsection \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent.\<close>
+subsection%unimportant \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent.\<close>
 
 lemma mem_is_interval_1_I:
   fixes a b c::real
@@ -6742,7 +6742,7 @@
   by (auto simp: is_interval_convex_1 convex_cball)
 
 
-subsection \<open>Another intermediate value theorem formulation\<close>
+subsection%unimportant \<open>Another intermediate value theorem formulation\<close>
 
 lemma ivt_increasing_component_on_1:
   fixes f :: "real \<Rightarrow> 'a::euclidean_space"
@@ -6787,7 +6787,7 @@
   by (rule ivt_decreasing_component_on_1) (auto simp: continuous_at_imp_continuous_on)
 
 
-subsection \<open>A bound within a convex hull, and so an interval\<close>
+subsection%unimportant \<open>A bound within a convex hull, and so an interval\<close>
 
 lemma convex_on_convex_hull_bound:
   assumes "convex_on (convex hull s) f"
@@ -6992,7 +6992,7 @@
     done
 qed
 
-subsubsection\<open>Representation of any interval as a finite convex hull\<close>
+subsubsection%unimportant\<open>Representation of any interval as a finite convex hull\<close>
 
 lemma image_stretch_interval:
   "(\<lambda>x. \<Sum>k\<in>Basis. (m k * (x\<bullet>k)) *\<^sub>R k) ` cbox a (b::'a::euclidean_space) =
@@ -7069,7 +7069,7 @@
 qed
 
 
-subsection \<open>Bounded convex function on open set is continuous\<close>
+subsection%unimportant \<open>Bounded convex function on open set is continuous\<close>
 
 lemma convex_on_bounded_continuous:
   fixes s :: "('a::real_normed_vector) set"
@@ -7186,7 +7186,7 @@
 qed
 
 
-subsection \<open>Upper bound on a ball implies upper and lower bounds\<close>
+subsection%unimportant \<open>Upper bound on a ball implies upper and lower bounds\<close>
 
 lemma convex_bounds_lemma:
   fixes x :: "'a::real_normed_vector"
@@ -7220,7 +7220,7 @@
 qed
 
 
-subsubsection \<open>Hence a convex function on an open set is continuous\<close>
+subsubsection%unimportant \<open>Hence a convex function on an open set is continuous\<close>
 
 lemma real_of_nat_ge_one_iff: "1 \<le> real (n::nat) \<longleftrightarrow> 1 \<le> n"
   by auto
diff -r 9c31678d2139 -r 0acdcd8f4ba1 src/HOL/Analysis/Euclidean_Space.thy
--- a/src/HOL/Analysis/Euclidean_Space.thy	Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Euclidean_Space.thy	Fri Apr 06 17:34:50 2018 +0200
@@ -12,7 +12,7 @@
 
 subsection \<open>Type class of Euclidean spaces\<close>
 
-class euclidean_space = real_inner +
+class%important euclidean_space = real_inner +
   fixes Basis :: "'a set"
   assumes nonempty_Basis [simp]: "Basis \<noteq> {}"
   assumes finite_Basis [simp]: "finite Basis"
@@ -152,7 +152,7 @@
     using False by (auto simp: inner_sum_left)
 qed
 
-subsection \<open>Subclass relationships\<close>
+subsection%unimportant \<open>Subclass relationships\<close>
 
 instance euclidean_space \<subseteq> perfect_space
 proof
@@ -175,9 +175,9 @@
 
 subsection \<open>Class instances\<close>
 
-subsubsection \<open>Type @{typ real}\<close>
+subsubsection%unimportant \<open>Type @{typ real}\<close>
 
-instantiation real :: euclidean_space
+instantiation%important real :: euclidean_space
 begin
 
 definition
@@ -191,9 +191,9 @@
 lemma DIM_real[simp]: "DIM(real) = 1"
   by simp
 
-subsubsection \<open>Type @{typ complex}\<close>
+subsubsection%unimportant \<open>Type @{typ complex}\<close>
 
-instantiation complex :: euclidean_space
+instantiation%important complex :: euclidean_space
 begin
 
 definition Basis_complex_def: "Basis = {1, \<i>}"
@@ -206,9 +206,9 @@
 lemma DIM_complex[simp]: "DIM(complex) = 2"
   unfolding Basis_complex_def by simp
 
-subsubsection \<open>Type @{typ "'a \<times> 'b"}\<close>
+subsubsection%unimportant \<open>Type @{typ "'a \<times> 'b"}\<close>
 
-instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
+instantiation%important prod :: (euclidean_space, euclidean_space) euclidean_space
 begin
 
 definition
diff -r 9c31678d2139 -r 0acdcd8f4ba1 src/HOL/Analysis/Inner_Product.thy
--- a/src/HOL/Analysis/Inner_Product.thy	Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Inner_Product.thy	Fri Apr 06 17:34:50 2018 +0200
@@ -27,7 +27,7 @@
 setup \<open>Sign.add_const_constraint
   (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
 
-class real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
+class%important real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
   fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
   assumes inner_commute: "inner x y = inner y x"
   and inner_add_left: "inner (x + y) z = inner x z + inner y z"
@@ -236,7 +236,7 @@
 
 subsection \<open>Class instances\<close>
 
-instantiation real :: real_inner
+instantiation%important real :: real_inner
 begin
 
 definition inner_real_def [simp]: "inner = ( * )"
@@ -265,7 +265,7 @@
     and real_inner_1_right[simp]: "inner x 1 = x"
   by simp_all
 
-instantiation complex :: real_inner
+instantiation%important complex :: real_inner
 begin
 
 definition inner_complex_def:
@@ -357,7 +357,7 @@
 
 subsection \<open>Gradient derivative\<close>
 
-definition
+definition%important
   gderiv ::
     "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
           ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
diff -r 9c31678d2139 -r 0acdcd8f4ba1 src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Fri Apr 06 17:34:50 2018 +0200
@@ -36,7 +36,7 @@
 
 subsection \<open>A generic notion of "hull" (convex, affine, conic hull and closure).\<close>
 
-definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "hull" 75)
+definition%important hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "hull" 75)
   where "S hull s = \<Inter>{t. S t \<and> s \<subseteq> t}"
 
 lemma hull_same: "S s \<Longrightarrow> S hull s = s"
@@ -109,10 +109,10 @@
 
 subsection \<open>Linear functions.\<close>
 
-lemma linear_iff:
+lemma%important linear_iff:
   "linear f \<longleftrightarrow> (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>R x) = c *\<^sub>R f x)"
   (is "linear f \<longleftrightarrow> ?rhs")
-proof
+proof%unimportant
   assume "linear f"
   then interpret f: linear f .
   show "?rhs" by (simp add: f.add f.scaleR)
@@ -230,11 +230,11 @@
 
 subsection \<open>Subspaces of vector spaces\<close>
 
-definition (in real_vector) subspace :: "'a set \<Rightarrow> bool"
+definition%important (in real_vector) subspace :: "'a set \<Rightarrow> bool"
   where "subspace S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>x \<in> S. \<forall>y \<in> S. x + y \<in> S) \<and> (\<forall>c. \<forall>x \<in> S. c *\<^sub>R x \<in> S)"
 
-definition (in real_vector) "span S = (subspace hull S)"
-definition (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span (S - {a}))"
+definition%important (in real_vector) "span S = (subspace hull S)"
+definition%important (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span (S - {a}))"
 abbreviation (in real_vector) "independent s \<equiv> \<not> dependent s"
 
 text \<open>Closure properties of subspaces.\<close>
@@ -284,7 +284,7 @@
  apply (metis add.assoc add.left_commute)
 using scaleR_add_right by blast
 
-subsection \<open>Properties of span\<close>
+subsection%unimportant \<open>Properties of span\<close>
 
 lemma (in real_vector) span_mono: "A \<subseteq> B \<Longrightarrow> span A \<subseteq> span B"
   by (metis span_def hull_mono)
@@ -1351,7 +1351,7 @@
 qed
 
 
-subsection \<open>More interesting properties of the norm.\<close>
+subsection%unimportant \<open>More interesting properties of the norm.\<close>
 
 lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
   by auto
@@ -1498,11 +1498,11 @@
 
 subsection \<open>Orthogonality.\<close>
 
+definition%important (in real_inner) "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"
+
 context real_inner
 begin
 
-definition "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"
-
 lemma orthogonal_self: "orthogonal x x \<longleftrightarrow> x = 0"
   by (simp add: orthogonal_def)
 
@@ -1567,7 +1567,7 @@
 
 subsection \<open>Bilinear functions.\<close>
 
-definition "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
+definition%important "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
 
 lemma bilinear_ladd: "bilinear h \<Longrightarrow> h (x + y) z = h x z + h y z"
   by (simp add: bilinear_def linear_iff)
@@ -1630,7 +1630,7 @@
 
 subsection \<open>Adjoints.\<close>
 
-definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
+definition%important "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
 
 lemma adjoint_unique:
   assumes "\<forall>x y. inner (f x) y = inner x (g y)"
@@ -1701,7 +1701,7 @@
   by (rule adjoint_unique, simp add: adjoint_clauses [OF lf])
 
 
-subsection \<open>Interlude: Some properties of real sets\<close>
+subsection%unimportant \<open>Interlude: Some properties of real sets\<close>
 
 lemma seq_mono_lemma:
   assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n"
@@ -1754,11 +1754,11 @@
 subsection \<open>Archimedean properties and useful consequences\<close>
 
 text\<open>Bernoulli's inequality\<close>
-proposition Bernoulli_inequality:
+proposition%important Bernoulli_inequality:
   fixes x :: real
   assumes "-1 \<le> x"
     shows "1 + n * x \<le> (1 + x) ^ n"
-proof (induct n)
+proof%unimportant (induct n)
   case 0
   then show ?case by simp
 next
@@ -1844,7 +1844,7 @@
   done
 
 
-subsection \<open>Euclidean Spaces as Typeclass\<close>
+subsection%unimportant \<open>Euclidean Spaces as Typeclass\<close>
 
 lemma independent_Basis: "independent Basis"
   unfolding dependent_def
@@ -1905,7 +1905,7 @@
 qed
 
 
-subsection \<open>Linearity and Bilinearity continued\<close>
+subsection%unimportant \<open>Linearity and Bilinearity continued\<close>
 
 lemma linear_bounded:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
@@ -2074,7 +2074,7 @@
 by (metis linear_imp_has_derivative differentiable_def)
 
 
-subsection \<open>We continue.\<close>
+subsection%unimportant \<open>We continue.\<close>
 
 lemma independent_bound:
   fixes S :: "'a::euclidean_space set"
@@ -2879,7 +2879,7 @@
 
 subsection \<open>Infinity norm\<close>
 
-definition "infnorm (x::'a::euclidean_space) = Sup {\<bar>x \<bullet> b\<bar> |b. b \<in> Basis}"
+definition%important "infnorm (x::'a::euclidean_space) = Sup {\<bar>x \<bullet> b\<bar> |b. b \<in> Basis}"
 
 lemma infnorm_set_image:
   fixes x :: "'a::euclidean_space"
@@ -3115,7 +3115,7 @@
 
 subsection \<open>Collinearity\<close>
 
-definition collinear :: "'a::real_vector set \<Rightarrow> bool"
+definition%important collinear :: "'a::real_vector set \<Rightarrow> bool"
   where "collinear S \<longleftrightarrow> (\<exists>u. \<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u)"
 
 lemma collinear_alt:
diff -r 9c31678d2139 -r 0acdcd8f4ba1 src/HOL/Analysis/Measurable.thy
--- a/src/HOL/Analysis/Measurable.thy	Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Measurable.thy	Fri Apr 06 17:34:50 2018 +0200
@@ -1,13 +1,13 @@
 (*  Title:      HOL/Analysis/Measurable.thy
     Author:     Johannes Hölzl <hoelzl@in.tum.de>
 *)
+section \<open>Measurability prover\<close>
 theory Measurable
   imports
     Sigma_Algebra
     "HOL-Library.Order_Continuity"
 begin
 
-subsection \<open>Measurability prover\<close>
 
 lemma (in algebra) sets_Collect_finite_All:
   assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S"
@@ -64,10 +64,10 @@
 attribute_setup measurable_cong = Measurable.cong_thm_attr
   "add congurence rules to measurability prover"
 
-method_setup measurable = \<open> Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \<close>
+method_setup%important measurable = \<open> Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \<close>
   "measurability prover"
 
-simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = \<open>K Measurable.simproc\<close>
+simproc_setup%important measurable ("A \<in> sets M" | "f \<in> measurable M N") = \<open>K Measurable.simproc\<close>
 
 setup \<open>
   Global_Theory.add_thms_dynamic (@{binding measurable}, Measurable.get_all)
@@ -380,7 +380,7 @@
   unfolding pred_def
   by (auto intro!: sets.sets_Collect_countable_All' sets.sets_Collect_countable_Ex' assms)
 
-subsection \<open>Measurability for (co)inductive predicates\<close>
+subsection%unimportant \<open>Measurability for (co)inductive predicates\<close>
 
 lemma measurable_bot[measurable]: "bot \<in> measurable M (count_space UNIV)"
   by (simp add: bot_fun_def)
diff -r 9c31678d2139 -r 0acdcd8f4ba1 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Measure_Space.thy	Fri Apr 06 17:34:50 2018 +0200
@@ -11,7 +11,7 @@
   Measurable "HOL-Library.Extended_Nonnegative_Real"
 begin
 
-subsection "Relate extended reals and the indicator function"
+subsection%unimportant "Relate extended reals and the indicator function"
 
 lemma suminf_cmult_indicator:
   fixes f :: "nat \<Rightarrow> ennreal"
@@ -59,7 +59,7 @@
   represent sigma algebras (with an arbitrary emeasure).
 \<close>
 
-subsection "Extend binary sets"
+subsection%unimportant "Extend binary sets"
 
 lemma LIMSEQ_binaryset:
   assumes f: "f {} = 0"
@@ -91,7 +91,7 @@
   shows "f {} = 0 \<Longrightarrow> (\<Sum>n. f (binaryset A B n)) = f A + f B"
   by (metis binaryset_sums sums_unique)
 
-subsection \<open>Properties of a premeasure @{term \<mu>}\<close>
+subsection%unimportant \<open>Properties of a premeasure @{term \<mu>}\<close>
 
 text \<open>
   The definitions for @{const positive} and @{const countably_additive} should be here, by they are
@@ -442,7 +442,7 @@
   using empty_continuous_imp_continuous_from_below[OF f fin] cont
   by blast
 
-subsection \<open>Properties of @{const emeasure}\<close>
+subsection%unimportant \<open>Properties of @{const emeasure}\<close>
 
 lemma emeasure_positive: "positive (sets M) (emeasure M)"
   by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def)
@@ -881,7 +881,7 @@
 
 subsection \<open>\<open>\<mu>\<close>-null sets\<close>
 
-definition null_sets :: "'a measure \<Rightarrow> 'a set set" where
+definition%important null_sets :: "'a measure \<Rightarrow> 'a set set" where
   "null_sets M = {N\<in>sets M. emeasure M N = 0}"
 
 lemma null_setsD1[dest]: "A \<in> null_sets M \<Longrightarrow> emeasure M A = 0"
@@ -989,7 +989,7 @@
 
 subsection \<open>The almost everywhere filter (i.e.\ quantifier)\<close>
 
-definition ae_filter :: "'a measure \<Rightarrow> 'a filter" where
+definition%important ae_filter :: "'a measure \<Rightarrow> 'a filter" where
   "ae_filter M = (INF N:null_sets M. principal (space M - N))"
 
 abbreviation almost_everywhere :: "'a measure \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
@@ -1265,7 +1265,7 @@
 
 subsection \<open>\<open>\<sigma>\<close>-finite Measures\<close>
 
-locale sigma_finite_measure =
+locale%important sigma_finite_measure =
   fixes M :: "'a measure"
   assumes sigma_finite_countable:
     "\<exists>A::'a set set. countable A \<and> A \<subseteq> sets M \<and> (\<Union>A) = space M \<and> (\<forall>a\<in>A. emeasure M a \<noteq> \<infinity>)"
@@ -1387,7 +1387,7 @@
 
 subsection \<open>Measure space induced by distribution of @{const measurable}-functions\<close>
 
-definition distr :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
+definition%important distr :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
   "distr M N f = measure_of (space N) (sets N) (\<lambda>A. emeasure M (f -` A \<inter> space M))"
 
 lemma
@@ -1513,12 +1513,12 @@
   "f \<in> measurable M N \<Longrightarrow> A \<in> null_sets (distr M N f) \<longleftrightarrow> f -` A \<inter> space M \<in> null_sets M \<and> A \<in> sets N"
   by (auto simp add: null_sets_def emeasure_distr)
 
-lemma distr_distr:
+lemma%important distr_distr:
   "g \<in> measurable N L \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> distr (distr M N f) L g = distr M L (g \<circ> f)"
   by (auto simp add: emeasure_distr measurable_space
            intro!: arg_cong[where f="emeasure M"] measure_eqI)
 
-subsection \<open>Real measure values\<close>
+subsection%unimportant \<open>Real measure values\<close>
 
 lemma ring_of_finite_sets: "ring_of_sets (space M) {A\<in>sets M. emeasure M A \<noteq> top}"
 proof (rule ring_of_setsI)
@@ -1705,7 +1705,7 @@
 
 subsection \<open>Set of measurable sets with finite measure\<close>
 
-definition fmeasurable :: "'a measure \<Rightarrow> 'a set set"
+definition%important fmeasurable :: "'a measure \<Rightarrow> 'a set set"
 where
   "fmeasurable M = {A\<in>sets M. emeasure M A < \<infinity>}"
 
@@ -1972,7 +1972,7 @@
 
 subsection \<open>Measure spaces with @{term "emeasure M (space M) < \<infinity>"}\<close>
 
-locale finite_measure = sigma_finite_measure M for M +
+locale%important finite_measure = sigma_finite_measure M for M +
   assumes finite_emeasure_space: "emeasure M (space M) \<noteq> top"
 
 lemma finite_measureI[Pure.intro!]:
@@ -2194,7 +2194,7 @@
     using bound[of x] sets_eq_imp_space_eq[OF sets] by (simp add: iter)
 qed (auto simp add: iter le_fun_def INF_apply[abs_def] intro!: meas cont)
 
-subsection \<open>Counting space\<close>
+subsection%unimportant \<open>Counting space\<close>
 
 lemma strict_monoI_Suc:
   assumes ord [simp]: "(\<And>n. f n < f (Suc n))" shows "strict_mono f"
@@ -2343,7 +2343,7 @@
   show "sigma_finite_measure (count_space A)" ..
 qed
 
-subsection \<open>Measure restricted to space\<close>
+subsection%unimportant \<open>Measure restricted to space\<close>
 
 lemma emeasure_restrict_space:
   assumes "\<Omega> \<inter> space M \<in> sets M" "A \<subseteq> \<Omega>"
@@ -2502,7 +2502,7 @@
   finally show "emeasure M X = emeasure N X" .
 qed fact
 
-subsection \<open>Null measure\<close>
+subsection%unimportant \<open>Null measure\<close>
 
 definition "null_measure M = sigma (space M) (sets M)"
 
@@ -2525,7 +2525,7 @@
 
 subsection \<open>Scaling a measure\<close>
 
-definition scale_measure :: "ennreal \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
+definition%important scale_measure :: "ennreal \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
 where
   "scale_measure r M = measure_of (space M) (sets M) (\<lambda>A. r * emeasure M A)"
 
@@ -2703,11 +2703,11 @@
   qed auto
 qed
 
-lemma unsigned_Hahn_decomposition:
+lemma%important unsigned_Hahn_decomposition:
   assumes [simp]: "sets N = sets M" and [measurable]: "A \<in> sets M"
     and [simp]: "emeasure M A \<noteq> top" "emeasure N A \<noteq> top"
   shows "\<exists>Y\<in>sets M. Y \<subseteq> A \<and> (\<forall>X\<in>sets M. X \<subseteq> Y \<longrightarrow> N X \<le> M X) \<and> (\<forall>X\<in>sets M. X \<subseteq> A \<longrightarrow> X \<inter> Y = {} \<longrightarrow> M X \<le> N X)"
-proof -
+proof%unimportant -
   have "\<exists>Y\<in>sets (restrict_space M A).
     (\<forall>X\<in>sets (restrict_space M A). X \<subseteq> Y \<longrightarrow> (restrict_space N A) X \<le> (restrict_space M A) X) \<and>
     (\<forall>X\<in>sets (restrict_space M A). X \<inter> Y = {} \<longrightarrow> (restrict_space M A) X \<le> (restrict_space N A) X)"
@@ -2728,12 +2728,12 @@
     done
 qed
 
-text \<open>
+text%important \<open>
   Define a lexicographical order on @{type measure}, in the order space, sets and measure. The parts
   of the lexicographical order are point-wise ordered.
 \<close>
 
-instantiation measure :: (type) order_bot
+instantiation%important measure :: (type) order_bot
 begin
 
 inductive less_eq_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
@@ -2746,10 +2746,10 @@
     if sets M = sets N then emeasure M \<le> emeasure N else sets M \<subseteq> sets N else space M \<subseteq> space N)"
   by (auto elim: less_eq_measure.cases intro: less_eq_measure.intros)
 
-definition less_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
+definition%important less_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
   "less_measure M N \<longleftrightarrow> (M \<le> N \<and> \<not> N \<le> M)"
 
-definition bot_measure :: "'a measure" where
+definition%important bot_measure :: "'a measure" where
   "bot_measure = sigma {} {}"
 
 lemma
@@ -2766,13 +2766,14 @@
 
 end
 
-lemma le_measure: "sets M = sets N \<Longrightarrow> M \<le> N \<longleftrightarrow> (\<forall>A\<in>sets M. emeasure M A \<le> emeasure N A)"
+lemma%important le_measure: "sets M = sets N \<Longrightarrow> M \<le> N \<longleftrightarrow> (\<forall>A\<in>sets M. emeasure M A \<le> emeasure N A)"
+  apply%unimportant -
   apply (auto simp: le_measure_iff le_fun_def dest: sets_eq_imp_space_eq)
   subgoal for X
     by (cases "X \<in> sets M") (auto simp: emeasure_notin_sets)
   done
 
-definition sup_measure' :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
+definition%important sup_measure' :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
 where
   "sup_measure' A B = measure_of (space A) (sets A) (\<lambda>X. SUP Y:sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
 
@@ -2900,7 +2901,7 @@
   qed
 qed simp_all
 
-definition sup_lexord :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b::order) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+definition%important sup_lexord :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b::order) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
 where
   "sup_lexord A B k s c =
     (if k A = k B then c else if \<not> k A \<le> k B \<and> \<not> k B \<le> k A then s else if k B \<le> k A then A else B)"
@@ -2926,10 +2927,10 @@
      (simp_all add: eq_commute[of _ "sets x"] le_measure_iff emeasure_sigma le_fun_def
                     sigma_sets_superset_generator sigma_sets_le_sets_iff)
 
-instantiation measure :: (type) semilattice_sup
+instantiation%important measure :: (type) semilattice_sup
 begin
 
-definition sup_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
+definition%important sup_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
 where
   "sup_measure A B =
     sup_lexord A B space (sigma (space A \<union> space B) {})
@@ -3057,7 +3058,7 @@
     by (simp add: A(3))
 qed
 
-instantiation measure :: (type) complete_lattice
+instantiation%important measure :: (type) complete_lattice
 begin
 
 interpretation sup_measure: comm_monoid_set sup "bot :: 'a measure"
@@ -3092,7 +3093,7 @@
   "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> sets i = sets M) \<Longrightarrow> sets (sup_measure.F id I) = sets M"
   by (induction I rule: finite_ne_induct) (simp_all add: sets_sup)
 
-definition Sup_measure' :: "'a measure set \<Rightarrow> 'a measure"
+definition%important Sup_measure' :: "'a measure set \<Rightarrow> 'a measure"
 where
   "Sup_measure' M = measure_of (\<Union>a\<in>M. space a) (\<Union>a\<in>M. sets a)
     (\<lambda>X. (SUP P:{P. finite P \<and> P \<subseteq> M }. sup_measure.F id P X))"
@@ -3163,20 +3164,20 @@
     using assms * by auto
 qed (rule UN_space_closed)
 
-definition Sup_measure :: "'a measure set \<Rightarrow> 'a measure"
+definition%important Sup_measure :: "'a measure set \<Rightarrow> 'a measure"
 where
   "Sup_measure = Sup_lexord space (Sup_lexord sets Sup_measure'
     (\<lambda>U. sigma (\<Union>u\<in>U. space u) (\<Union>u\<in>U. sets u))) (\<lambda>U. sigma (\<Union>u\<in>U. space u) {})"
 
-definition Inf_measure :: "'a measure set \<Rightarrow> 'a measure"
+definition%important Inf_measure :: "'a measure set \<Rightarrow> 'a measure"
 where
   "Inf_measure A = Sup {x. \<forall>a\<in>A. x \<le> a}"
 
-definition inf_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
+definition%important inf_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
 where
   "inf_measure a b = Inf {a, b}"
 
-definition top_measure :: "'a measure"
+definition%important top_measure :: "'a measure"
 where
   "top_measure = Inf {}"
 
@@ -3417,7 +3418,7 @@
   qed
 qed
 
-subsubsection \<open>Supremum of a set of $\sigma$-algebras\<close>
+subsubsection%unimportant \<open>Supremum of a set of $\sigma$-algebras\<close>
 
 lemma space_Sup_eq_UN: "space (Sup M) = (\<Union>x\<in>M. space x)"
   unfolding Sup_measure_def
diff -r 9c31678d2139 -r 0acdcd8f4ba1 src/HOL/Analysis/Norm_Arith.thy
--- a/src/HOL/Analysis/Norm_Arith.thy	Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Norm_Arith.thy	Fri Apr 06 17:34:50 2018 +0200
@@ -131,14 +131,14 @@
 
 ML_file "normarith.ML"
 
-method_setup norm = \<open>
+method_setup%important norm = \<open>
   Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
 \<close> "prove simple linear statements about vector norms"
 
 
 text \<open>Hence more metric properties.\<close>
 
-lemma dist_triangle_add:
+lemma%important dist_triangle_add:
   fixes x y x' y' :: "'a::real_normed_vector"
   shows "dist (x + y) (x' + y') \<le> dist x x' + dist y y'"
   by norm
diff -r 9c31678d2139 -r 0acdcd8f4ba1 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Path_Connected.thy	Fri Apr 06 17:34:50 2018 +0200
@@ -10,34 +10,34 @@
 
 subsection \<open>Paths and Arcs\<close>
 
-definition path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
+definition%important path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
   where "path g \<longleftrightarrow> continuous_on {0..1} g"
 
-definition pathstart :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
+definition%important pathstart :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
   where "pathstart g = g 0"
 
-definition pathfinish :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
+definition%important pathfinish :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
   where "pathfinish g = g 1"
 
-definition path_image :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a set"
+definition%important path_image :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a set"
   where "path_image g = g ` {0 .. 1}"
 
-definition reversepath :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a"
+definition%important reversepath :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a"
   where "reversepath g = (\<lambda>x. g(1 - x))"
 
-definition joinpaths :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a"
+definition%important joinpaths :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a"
     (infixr "+++" 75)
   where "g1 +++ g2 = (\<lambda>x. if x \<le> 1/2 then g1 (2 * x) else g2 (2 * x - 1))"
 
-definition simple_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
+definition%important simple_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
   where "simple_path g \<longleftrightarrow>
      path g \<and> (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. g x = g y \<longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0)"
 
-definition arc :: "(real \<Rightarrow> 'a :: topological_space) \<Rightarrow> bool"
+definition%important arc :: "(real \<Rightarrow> 'a :: topological_space) \<Rightarrow> bool"
   where "arc g \<longleftrightarrow> path g \<and> inj_on g {0..1}"
 
 
-subsection\<open>Invariance theorems\<close>
+subsection%unimportant\<open>Invariance theorems\<close>
 
 lemma path_eq: "path p \<Longrightarrow> (\<And>t. t \<in> {0..1} \<Longrightarrow> p t = q t) \<Longrightarrow> path q"
   using continuous_on_eq path_def by blast
@@ -132,7 +132,7 @@
   using assms inj_on_eq_iff [of f]
   by (auto simp: arc_def inj_on_def path_linear_image_eq)
 
-subsection\<open>Basic lemmas about paths\<close>
+subsection%unimportant\<open>Basic lemmas about paths\<close>
 
 lemma continuous_on_path: "path f \<Longrightarrow> t \<subseteq> {0..1} \<Longrightarrow> continuous_on t f"
   using continuous_on_subset path_def by blast
@@ -301,7 +301,7 @@
     done
 qed
 
-section \<open>Path Images\<close>
+section%unimportant \<open>Path Images\<close>
 
 lemma bounded_path_image: "path g \<Longrightarrow> bounded(path_image g)"
   by (simp add: compact_imp_bounded compact_path_image)
@@ -394,7 +394,7 @@
   by (auto simp: simple_path_def path_image_def inj_on_def less_eq_real_def Ball_def)
 
 
-subsection\<open>Simple paths with the endpoints removed\<close>
+subsection%unimportant\<open>Simple paths with the endpoints removed\<close>
 
 lemma simple_path_endless:
     "simple_path c \<Longrightarrow> path_image c - {pathstart c,pathfinish c} = c ` {0<..<1}"
@@ -417,7 +417,7 @@
   by (simp add: simple_path_endless)
 
 
-subsection\<open>The operations on paths\<close>
+subsection%unimportant\<open>The operations on paths\<close>
 
 lemma path_image_subset_reversepath: "path_image(reversepath g) \<le> path_image g"
   by (auto simp: path_image_def reversepath_def)
@@ -565,7 +565,7 @@
   by (rule ext) (auto simp: mult.commute)
 
 
-subsection\<open>Some reversed and "if and only if" versions of joining theorems\<close>
+subsection%unimportant\<open>Some reversed and "if and only if" versions of joining theorems\<close>
 
 lemma path_join_path_ends:
   fixes g1 :: "real \<Rightarrow> 'a::metric_space"
@@ -698,7 +698,7 @@
 using pathfinish_in_path_image by (fastforce simp: arc_join_eq)
 
 
-subsection\<open>The joining of paths is associative\<close>
+subsection%unimportant\<open>The joining of paths is associative\<close>
 
 lemma path_assoc:
     "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart r\<rbrakk>
@@ -748,7 +748,7 @@
       \<Longrightarrow> arc(p +++ (q +++ r)) \<longleftrightarrow> arc((p +++ q) +++ r)"
 by (simp add: arc_simple_path simple_path_assoc)
 
-subsubsection\<open>Symmetry and loops\<close>
+subsubsection%unimportant\<open>Symmetry and loops\<close>
 
 lemma path_sym:
     "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> path(p +++ q) \<longleftrightarrow> path(q +++ p)"
@@ -767,7 +767,7 @@
 
 section\<open>Choosing a subpath of an existing path\<close>
 
-definition subpath :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a::real_normed_vector"
+definition%important subpath :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a::real_normed_vector"
   where "subpath a b g \<equiv> \<lambda>x. g((b - a) * x + a)"
 
 lemma path_image_subpath_gen:
@@ -945,7 +945,7 @@
 lemma join_subpaths_middle: "subpath (0) ((1 / 2)) p +++ subpath ((1 / 2)) 1 p = p"
   by (rule ext) (simp add: joinpaths_def subpath_def divide_simps)
 
-subsection\<open>There is a subpath to the frontier\<close>
+subsection%unimportant\<open>There is a subpath to the frontier\<close>
 
 lemma subpath_to_frontier_explicit:
     fixes S :: "'a::metric_space set"
@@ -1063,7 +1063,7 @@
 
 subsection \<open>shiftpath: Reparametrizing a closed curve to start at some chosen point\<close>
 
-definition shiftpath :: "real \<Rightarrow> (real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a"
+definition%important shiftpath :: "real \<Rightarrow> (real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a"
   where "shiftpath a f = (\<lambda>x. if (a + x) \<le> 1 then f (a + x) else f (a + x - 1))"
 
 lemma pathstart_shiftpath: "a \<le> 1 \<Longrightarrow> pathstart (shiftpath a g) = g a"
@@ -1179,7 +1179,7 @@
 
 subsection \<open>Special case of straight-line paths\<close>
 
-definition linepath :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real \<Rightarrow> 'a"
+definition%important linepath :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real \<Rightarrow> 'a"
   where "linepath a b = (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b)"
 
 lemma pathstart_linepath[simp]: "pathstart (linepath a b) = a"
@@ -1259,7 +1259,7 @@
 qed
 
 
-subsection\<open>Segments via convex hulls\<close>
+subsection%unimportant\<open>Segments via convex hulls\<close>
 
 lemma segments_subset_convex_hull:
     "closed_segment a b \<subseteq> (convex hull {a,b,c})"
@@ -1379,7 +1379,7 @@
     by (force simp: inj_on_def)
 qed
 
-subsection \<open>Bounding a point away from a path\<close>
+subsection%unimportant \<open>Bounding a point away from a path\<close>
 
 lemma not_on_path_ball:
   fixes g :: "real \<Rightarrow> 'a::heine_borel"
@@ -1416,10 +1416,10 @@
 
 section \<open>Path component, considered as a "joinability" relation (from Tom Hales)\<close>
 
-definition "path_component s x y \<longleftrightarrow>
+definition%important "path_component s x y \<longleftrightarrow>
   (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)"
 
-abbreviation
+abbreviation%important
    "path_component_set s x \<equiv> Collect (path_component s x)"
 
 lemmas path_defs = path_def pathstart_def pathfinish_def path_image_def path_component_def
@@ -1471,7 +1471,7 @@
   done
 
 
-subsubsection \<open>Path components as sets\<close>
+subsubsection%unimportant \<open>Path components as sets\<close>
 
 lemma path_component_set:
   "path_component_set s x =
@@ -1495,7 +1495,7 @@
 
 subsection \<open>Path connectedness of a space\<close>
 
-definition "path_connected s \<longleftrightarrow>
+definition%important "path_connected s \<longleftrightarrow>
   (\<forall>x\<in>s. \<forall>y\<in>s. \<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)"
 
 lemma path_connected_component: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. path_component s x y)"
@@ -1806,7 +1806,7 @@
     using path_component_eq_empty by auto
 qed
 
-subsection\<open>Lemmas about path-connectedness\<close>
+subsection%unimportant\<open>Lemmas about path-connectedness\<close>
 
 lemma path_connected_linear_image:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
@@ -1878,7 +1878,7 @@
 using is_interval_connected_1 is_interval_path_connected path_connected_imp_connected by blast
 
 
-subsection\<open>Path components\<close>
+subsection%unimportant\<open>Path components\<close>
 
 lemma Union_path_component [simp]:
    "Union {path_component_set S x |x. x \<in> S} = S"
@@ -1990,11 +1990,11 @@
   "2 \<le> DIM('N::euclidean_space) \<Longrightarrow> connected(- {a::'N})"
   by (simp add: path_connected_punctured_universe path_connected_imp_connected)
 
-lemma path_connected_sphere:
+lemma%important path_connected_sphere:
   fixes a :: "'a :: euclidean_space"
   assumes "2 \<le> DIM('a)"
   shows "path_connected(sphere a r)"
-proof (cases r "0::real" rule: linorder_cases)
+proof%unimportant (cases r "0::real" rule: linorder_cases)
   case less
   then show ?thesis
     by (simp add: path_connected_empty)
@@ -2315,26 +2315,26 @@
     using path_connected_translation by metis
 qed
 
-lemma path_connected_annulus:
+lemma%important path_connected_annulus:
   fixes a :: "'N::euclidean_space"
   assumes "2 \<le> DIM('N)"
   shows "path_connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
         "path_connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
         "path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
         "path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> r2}"
-  by (auto simp: is_interval_def intro!: is_interval_convex convex_imp_path_connected path_connected_2DIM_I [OF assms])
-
-lemma connected_annulus:
+  by%unimportant (auto simp: is_interval_def intro!: is_interval_convex convex_imp_path_connected path_connected_2DIM_I [OF assms])
+
+lemma%important connected_annulus:
   fixes a :: "'N::euclidean_space"
   assumes "2 \<le> DIM('N::euclidean_space)"
   shows "connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
         "connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
         "connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
         "connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> r2}"
-  by (auto simp: path_connected_annulus [OF assms] path_connected_imp_connected)
-
-
-subsection\<open>Relations between components and path components\<close>
+  by%unimportant (auto simp: path_connected_annulus [OF assms] path_connected_imp_connected)
+
+
+subsection%unimportant\<open>Relations between components and path components\<close>
 
 lemma open_connected_component:
   fixes s :: "'a::real_normed_vector set"
@@ -2439,7 +2439,7 @@
 qed
 
 
-subsection\<open>Existence of unbounded components\<close>
+subsection%unimportant\<open>Existence of unbounded components\<close>
 
 lemma cobounded_unbounded_component:
     fixes s :: "'a :: euclidean_space set"
@@ -2527,13 +2527,13 @@
 
 section\<open>The "inside" and "outside" of a set\<close>
 
-text\<open>The inside comprises the points in a bounded connected component of the set's complement.
+text%important\<open>The inside comprises the points in a bounded connected component of the set's complement.
   The outside comprises the points in unbounded connected component of the complement.\<close>
 
-definition inside where
+definition%important inside where
   "inside s \<equiv> {x. (x \<notin> s) \<and> bounded(connected_component_set ( - s) x)}"
 
-definition outside where
+definition%important outside where
   "outside s \<equiv> -s \<inter> {x. ~ bounded(connected_component_set (- s) x)}"
 
 lemma outside: "outside s = {x. ~ bounded(connected_component_set (- s) x)}"
@@ -3329,14 +3329,14 @@
 
 subsection\<open>Condition for an open map's image to contain a ball\<close>
 
-lemma ball_subset_open_map_image:
+lemma%important ball_subset_open_map_image:
   fixes f :: "'a::heine_borel \<Rightarrow> 'b :: {real_normed_vector,heine_borel}"
   assumes contf: "continuous_on (closure S) f"
       and oint: "open (f ` interior S)"
       and le_no: "\<And>z. z \<in> frontier S \<Longrightarrow> r \<le> norm(f z - f a)"
       and "bounded S" "a \<in> S" "0 < r"
     shows "ball (f a) r \<subseteq> f ` S"
-proof (cases "f ` S = UNIV")
+proof%unimportant (cases "f ` S = UNIV")
   case True then show ?thesis by simp
 next
   case False
@@ -3382,10 +3382,10 @@
 
 section\<open> Homotopy of maps p,q : X=>Y with property P of all intermediate maps.\<close>
 
-text\<open> We often just want to require that it fixes some subset, but to take in
+text%important\<open> We often just want to require that it fixes some subset, but to take in
   the case of a loop homotopy, it's convenient to have a general property P.\<close>
 
-definition homotopic_with ::
+definition%important homotopic_with ::
   "[('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> bool, 'a set, 'b set, 'a \<Rightarrow> 'b, 'a \<Rightarrow> 'b] \<Rightarrow> bool"
 where
  "homotopic_with P X Y p q \<equiv>
@@ -3487,7 +3487,7 @@
 qed
 
 
-subsection\<open> Trivial properties.\<close>
+subsection%unimportant\<open> Trivial properties.\<close>
 
 lemma homotopic_with_imp_property: "homotopic_with P X Y f g \<Longrightarrow> P f \<and> P g"
   unfolding homotopic_with_def Ball_def
@@ -3745,7 +3745,7 @@
 subsection\<open>Homotopy of paths, maintaining the same endpoints.\<close>
 
 
-definition homotopic_paths :: "['a set, real \<Rightarrow> 'a, real \<Rightarrow> 'a::topological_space] \<Rightarrow> bool"
+definition%important homotopic_paths :: "['a set, real \<Rightarrow> 'a, real \<Rightarrow> 'a::topological_space] \<Rightarrow> bool"
   where
      "homotopic_paths s p q \<equiv>
        homotopic_with (\<lambda>r. pathstart r = pathstart p \<and> pathfinish r = pathfinish p) {0..1} s p q"
@@ -3897,28 +3897,28 @@
 
 subsection\<open>Group properties for homotopy of paths\<close>
 
-text\<open>So taking equivalence classes under homotopy would give the fundamental group\<close>
-
-proposition homotopic_paths_rid:
+text%important\<open>So taking equivalence classes under homotopy would give the fundamental group\<close>
+
+proposition%important homotopic_paths_rid:
     "\<lbrakk>path p; path_image p \<subseteq> s\<rbrakk> \<Longrightarrow> homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p)) p"
-  apply (subst homotopic_paths_sym)
+  apply%unimportant (subst homotopic_paths_sym)
   apply (rule homotopic_paths_reparametrize [where f = "\<lambda>t. if  t \<le> 1 / 2 then 2 *\<^sub>R t else 1"])
   apply (simp_all del: le_divide_eq_numeral1)
   apply (subst split_01)
   apply (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def)+
   done
 
-proposition homotopic_paths_lid:
+proposition%important homotopic_paths_lid:
    "\<lbrakk>path p; path_image p \<subseteq> s\<rbrakk> \<Longrightarrow> homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p) p"
-using homotopic_paths_rid [of "reversepath p" s]
+using%unimportant homotopic_paths_rid [of "reversepath p" s]
   by (metis homotopic_paths_reversepath path_image_reversepath path_reversepath pathfinish_linepath
         pathfinish_reversepath reversepath_joinpaths reversepath_linepath)
 
-proposition homotopic_paths_assoc:
+proposition%important homotopic_paths_assoc:
    "\<lbrakk>path p; path_image p \<subseteq> s; path q; path_image q \<subseteq> s; path r; path_image r \<subseteq> s; pathfinish p = pathstart q;
      pathfinish q = pathstart r\<rbrakk>
     \<Longrightarrow> homotopic_paths s (p +++ (q +++ r)) ((p +++ q) +++ r)"
-  apply (subst homotopic_paths_sym)
+  apply%unimportant (subst homotopic_paths_sym)
   apply (rule homotopic_paths_reparametrize
            [where f = "\<lambda>t. if  t \<le> 1 / 2 then inverse 2 *\<^sub>R t
                            else if  t \<le> 3 / 4 then t - (1 / 4)
@@ -3929,10 +3929,10 @@
   apply (auto simp: joinpaths_def)
   done
 
-proposition homotopic_paths_rinv:
+proposition%important homotopic_paths_rinv:
   assumes "path p" "path_image p \<subseteq> s"
     shows "homotopic_paths s (p +++ reversepath p) (linepath (pathstart p) (pathstart p))"
-proof -
+proof%unimportant -
   have "continuous_on ({0..1} \<times> {0..1}) (\<lambda>x. (subpath 0 (fst x) p +++ reversepath (subpath 0 (fst x) p)) (snd x))"
     using assms
     apply (simp add: joinpaths_def subpath_def reversepath_def path_def del: le_divide_eq_numeral1)
@@ -3952,15 +3952,15 @@
     done
 qed
 
-proposition homotopic_paths_linv:
+proposition%important homotopic_paths_linv:
   assumes "path p" "path_image p \<subseteq> s"
     shows "homotopic_paths s (reversepath p +++ p) (linepath (pathfinish p) (pathfinish p))"
-using homotopic_paths_rinv [of "reversepath p" s] assms by simp
+using%unimportant homotopic_paths_rinv [of "reversepath p" s] assms by simp
 
 
 subsection\<open> Homotopy of loops without requiring preservation of endpoints.\<close>
 
-definition homotopic_loops :: "'a::topological_space set \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool"  where
+definition%important homotopic_loops :: "'a::topological_space set \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool"  where
  "homotopic_loops s p q \<equiv>
      homotopic_with (\<lambda>r. pathfinish r = pathstart r) {0..1} s p q"
 
@@ -4025,14 +4025,14 @@
 
 subsection\<open>Relations between the two variants of homotopy\<close>
 
-proposition homotopic_paths_imp_homotopic_loops:
+proposition%important homotopic_paths_imp_homotopic_loops:
     "\<lbrakk>homotopic_paths s p q; pathfinish p = pathstart p; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> homotopic_loops s p q"
-  by (auto simp: homotopic_paths_def homotopic_loops_def intro: homotopic_with_mono)
-
-proposition homotopic_loops_imp_homotopic_paths_null:
+  by%unimportant (auto simp: homotopic_paths_def homotopic_loops_def intro: homotopic_with_mono)
+
+proposition%important homotopic_loops_imp_homotopic_paths_null:
   assumes "homotopic_loops s p (linepath a a)"
     shows "homotopic_paths s p (linepath (pathstart p) (pathstart p))"
-proof -
+proof%unimportant -
   have "path p" by (metis assms homotopic_loops_imp_path)
   have ploop: "pathfinish p = pathstart p" by (metis assms homotopic_loops_imp_loop)
   have pip: "path_image p \<subseteq> s" by (metis assms homotopic_loops_imp_subset)
@@ -4100,12 +4100,12 @@
     by (blast intro: homotopic_paths_trans)
 qed
 
-proposition homotopic_loops_conjugate:
+proposition%important homotopic_loops_conjugate:
   fixes s :: "'a::real_normed_vector set"
   assumes "path p" "path q" and pip: "path_image p \<subseteq> s" and piq: "path_image q \<subseteq> s"
       and papp: "pathfinish p = pathstart q" and qloop: "pathfinish q = pathstart q"
     shows "homotopic_loops s (p +++ q +++ reversepath p) q"
-proof -
+proof%unimportant -
   have contp: "continuous_on {0..1} p"  using \<open>path p\<close> [unfolded path_def] by blast
   have contq: "continuous_on {0..1} q"  using \<open>path q\<close> [unfolded path_def] by blast
   have c1: "continuous_on ({0..1} \<times> {0..1}) (\<lambda>x. p ((1 - fst x) * snd x + fst x))"
@@ -4197,7 +4197,7 @@
 qed
 
 
-subsection\<open> Homotopy of "nearby" function, paths and loops.\<close>
+subsection%unimportant\<open> Homotopy of "nearby" function, paths and loops.\<close>
 
 lemma homotopic_with_linear:
   fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
@@ -4358,10 +4358,10 @@
     using homotopic_join_subpaths2 by blast
 qed
 
-proposition homotopic_join_subpaths:
+proposition%important homotopic_join_subpaths:
    "\<lbrakk>path g; path_image g \<subseteq> s; u \<in> {0..1}; v \<in> {0..1}; w \<in> {0..1}\<rbrakk>
     \<Longrightarrow> homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
-apply (rule le_cases3 [of u v w])
+apply%unimportant (rule le_cases3 [of u v w])
 using homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3 by metis+
 
 text\<open>Relating homotopy of trivial loops to path-connectedness.\<close>
@@ -4399,9 +4399,9 @@
 
 subsection\<open>Simply connected sets\<close>
 
-text\<open>defined as "all loops are homotopic (as loops)\<close>
-
-definition simply_connected where
+text%important\<open>defined as "all loops are homotopic (as loops)\<close>
+
+definition%important simply_connected where
   "simply_connected S \<equiv>
         \<forall>p q. path p \<and> pathfinish p = pathstart p \<and> path_image p \<subseteq> S \<and>
               path q \<and> pathfinish q = pathstart q \<and> path_image q \<subseteq> S
@@ -4583,7 +4583,7 @@
 
 subsection\<open>Contractible sets\<close>
 
-definition contractible where
+definition%important contractible where
  "contractible S \<equiv> \<exists>a. homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
 
 proposition contractible_imp_simply_connected:
@@ -4846,7 +4846,7 @@
 
 subsection\<open>Local versions of topological properties in general\<close>
 
-definition locally :: "('a::topological_space set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
+definition%important locally :: "('a::topological_space set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
 where
  "locally P S \<equiv>
         \<forall>w x. openin (subtopology euclidean S) w \<and> x \<in> w
@@ -5077,7 +5077,7 @@
 
 subsection\<open>Sort of induction principle for connected sets\<close>
 
-lemma connected_induction:
+lemma%important connected_induction:
   assumes "connected S"
       and opD: "\<And>T a. \<lbrakk>openin (subtopology euclidean S) T; a \<in> T\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> T \<and> P z"
       and opI: "\<And>a. a \<in> S
@@ -5085,7 +5085,7 @@
                      (\<forall>x \<in> T. \<forall>y \<in> T. P x \<and> P y \<and> Q x \<longrightarrow> Q y)"
       and etc: "a \<in> S" "b \<in> S" "P a" "P b" "Q a"
     shows "Q b"
-proof -
+proof%unimportant -
   have 1: "openin (subtopology euclidean S)
              {b. \<exists>T. openin (subtopology euclidean S) T \<and>
                      b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> Q x)}"
@@ -5176,14 +5176,14 @@
 
 subsection\<open>Basic properties of local compactness\<close>
 
-lemma locally_compact:
+lemma%important locally_compact:
   fixes s :: "'a :: metric_space set"
   shows
     "locally compact s \<longleftrightarrow>
      (\<forall>x \<in> s. \<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and>
                     openin (subtopology euclidean s) u \<and> compact v)"
      (is "?lhs = ?rhs")
-proof
+proof%unimportant
   assume ?lhs
   then show ?rhs
     apply clarify
@@ -5730,12 +5730,12 @@
     by (metis \<open>U = S \<inter> V\<close> inf.bounded_iff openin_imp_subset that)
 qed
 
-corollary Sura_Bura:
+corollary%important Sura_Bura:
   fixes S :: "'a::euclidean_space set"
   assumes "locally compact S" "C \<in> components S" "compact C"
   shows "C = \<Inter> {K. C \<subseteq> K \<and> compact K \<and> openin (subtopology euclidean S) K}"
          (is "C = ?rhs")
-proof
+proof%unimportant
   show "?rhs \<subseteq> C"
   proof (clarsimp, rule ccontr)
     fix x
@@ -5865,17 +5865,17 @@
     by (metis assms(1) assms(2) assms(3) mem_Collect_eq path_component_subset path_connected_path_component)
 qed
 
-proposition locally_path_connected:
+proposition%important locally_path_connected:
   "locally path_connected S \<longleftrightarrow>
    (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
           \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v))"
-by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
-
-proposition locally_path_connected_open_path_component:
+by%unimportant (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
+
+proposition%important locally_path_connected_open_path_component:
   "locally path_connected S \<longleftrightarrow>
    (\<forall>t x. openin (subtopology euclidean S) t \<and> x \<in> t
           \<longrightarrow> openin (subtopology euclidean S) (path_component_set t x))"
-by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
+by%unimportant (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
 
 lemma locally_connected_open_component:
   "locally connected S \<longleftrightarrow>
@@ -5883,14 +5883,14 @@
           \<longrightarrow> openin (subtopology euclidean S) c)"
 by (metis components_iff locally_connected_open_connected_component)
 
-proposition locally_connected_im_kleinen:
+proposition%important locally_connected_im_kleinen:
   "locally connected S \<longleftrightarrow>
    (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
        \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and>
                 x \<in> u \<and> u \<subseteq> v \<and>
                 (\<forall>y. y \<in> u \<longrightarrow> (\<exists>c. connected c \<and> c \<subseteq> v \<and> x \<in> c \<and> y \<in> c))))"
    (is "?lhs = ?rhs")
-proof
+proof%unimportant
   assume ?lhs
   then show ?rhs
     by (fastforce simp add: locally_connected)
@@ -5924,7 +5924,7 @@
     done
 qed
 
-proposition locally_path_connected_im_kleinen:
+proposition%important locally_path_connected_im_kleinen:
   "locally path_connected S \<longleftrightarrow>
    (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
        \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and>
@@ -5932,7 +5932,7 @@
                 (\<forall>y. y \<in> u \<longrightarrow> (\<exists>p. path p \<and> path_image p \<subseteq> v \<and>
                                 pathstart p = x \<and> pathfinish p = y))))"
    (is "?lhs = ?rhs")
-proof
+proof%unimportant
   assume ?lhs
   then show ?rhs
     apply (simp add: locally_path_connected path_connected_def)
@@ -6082,13 +6082,13 @@
   shows "open S \<Longrightarrow> path_component_set S x = connected_component_set S x"
 by (simp add: open_path_connected_component)
 
-proposition locally_connected_quotient_image:
+proposition%important locally_connected_quotient_image:
   assumes lcS: "locally connected S"
       and oo: "\<And>T. T \<subseteq> f ` S
                 \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow>
                     openin (subtopology euclidean (f ` S)) T"
     shows "locally connected (f ` S)"
-proof (clarsimp simp: locally_connected_open_component)
+proof%unimportant (clarsimp simp: locally_connected_open_component)
   fix U C
   assume opefSU: "openin (subtopology euclidean (f ` S)) U" and "C \<in> components U"
   then have "C \<subseteq> U" "U \<subseteq> f ` S"
@@ -6148,12 +6148,12 @@
 qed
 
 text\<open>The proof resembles that above but is not identical!\<close>
-proposition locally_path_connected_quotient_image:
+proposition%important locally_path_connected_quotient_image:
   assumes lcS: "locally path_connected S"
       and oo: "\<And>T. T \<subseteq> f ` S
                 \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow> openin (subtopology euclidean (f ` S)) T"
     shows "locally path_connected (f ` S)"
-proof (clarsimp simp: locally_path_connected_open_path_component)
+proof%unimportant (clarsimp simp: locally_path_connected_open_path_component)
   fix U y
   assume opefSU: "openin (subtopology euclidean (f ` S)) U" and "y \<in> U"
   then have "path_component_set U y \<subseteq> U" "U \<subseteq> f ` S"
@@ -6221,7 +6221,7 @@
     by metis
 qed
 
-subsection\<open>Components, continuity, openin, closedin\<close>
+subsection%unimportant\<open>Components, continuity, openin, closedin\<close>
 
 lemma continuous_on_components_gen:
  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
@@ -6324,7 +6324,8 @@
   fixes S :: "'a::real_normed_vector set"
   assumes S: "closed S" and c: " c \<in> components(-S)"
     shows "closed (S \<union> c)"
-by (metis Compl_eq_Diff_UNIV S c closed_closedin closedin_Un_complement_component locally_connected_UNIV subtopology_UNIV)
+  by (metis Compl_eq_Diff_UNIV S c closed_closedin closedin_Un_complement_component
+      locally_connected_UNIV subtopology_UNIV)
 
 
 subsection\<open>Existence of isometry between subspaces of same dimension\<close>
@@ -6381,7 +6382,7 @@
     by (rule that [OF \<open>linear f\<close> \<open>f ` S \<subseteq> T\<close>])
 qed
 
-proposition isometries_subspaces:
+proposition%important isometries_subspaces:
   fixes S :: "'a::euclidean_space set"
     and T :: "'b::euclidean_space set"
   assumes S: "subspace S"
@@ -6392,7 +6393,7 @@
                     "\<And>x. x \<in> T \<Longrightarrow> norm(g x) = norm x"
                     "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
                     "\<And>x. x \<in> T \<Longrightarrow> f(g x) = x"
-proof -
+proof%unimportant -
   obtain B where "B \<subseteq> S" and Borth: "pairwise orthogonal B"
              and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
              and "independent B" "finite B" "card B = dim S" "span B = S"
@@ -6549,7 +6550,7 @@
 
 subsection\<open>Retracts, in a general sense, preserve (co)homotopic triviality)\<close>
 
-locale Retracts =
+locale%important Retracts =
   fixes s h t k
   assumes conth: "continuous_on s h"
       and imh: "h ` s = t"
@@ -6715,7 +6716,7 @@
 
 subsection\<open>Homotopy equivalence\<close>
 
-definition homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
+definition%important homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
              (infix "homotopy'_eqv" 50)
   where "S homotopy_eqv T \<equiv>
         \<exists>f g. continuous_on S f \<and> f ` S \<subseteq> T \<and>
@@ -7003,7 +7004,7 @@
   shows "\<lbrakk>contractible S; S homeomorphic T\<rbrakk> \<Longrightarrow> contractible T"
   by (metis homeomorphic_contractible_eq)
 
-subsection\<open>Misc other results\<close>
+subsection%unimportant\<open>Misc other results\<close>
 
 lemma bounded_connected_Compl_real:
   fixes S :: "real set"
@@ -7047,7 +7048,7 @@
     by blast
 qed
 
-subsection\<open>Some Uncountable Sets\<close>
+subsection%unimportant\<open>Some Uncountable Sets\<close>
 
 lemma uncountable_closed_segment:
   fixes a :: "'a::real_normed_vector"
@@ -7186,7 +7187,7 @@
   by (simp add: arc_imp_simple_path assms simple_path_image_uncountable)
 
 
-subsection\<open> Some simple positive connection theorems\<close>
+subsection%unimportant\<open> Some simple positive connection theorems\<close>
 
 proposition path_connected_convex_diff_countable:
   fixes U :: "'a::euclidean_space set"
@@ -7453,7 +7454,7 @@
 
 subsection\<open> Self-homeomorphisms shuffling points about in various ways.\<close>
 
-subsubsection\<open>The theorem \<open>homeomorphism_moving_points_exists\<close>\<close>
+subsubsection%unimportant\<open>The theorem \<open>homeomorphism_moving_points_exists\<close>\<close>
 
 lemma homeomorphism_moving_point_1:
   fixes a :: "'a::euclidean_space"
@@ -7845,7 +7846,7 @@
   qed
 qed
 
-proposition homeomorphism_moving_points_exists:
+proposition%important homeomorphism_moving_points_exists:
   fixes S :: "'a::euclidean_space set"
   assumes 2: "2 \<le> DIM('a)" "open S" "connected S" "S \<subseteq> T" "finite K"
       and KS: "\<And>i. i \<in> K \<Longrightarrow> x i \<in> S \<and> y i \<in> S"
@@ -7853,7 +7854,7 @@
       and S: "S \<subseteq> T" "T \<subseteq> affine hull S" "connected S"
   obtains f g where "homeomorphism T T f g" "\<And>i. i \<in> K \<Longrightarrow> f(x i) = y i"
                     "{x. ~ (f x = x \<and> g x = x)} \<subseteq> S" "bounded {x. (~ (f x = x \<and> g x = x))}"
-proof (cases "S = {}")
+proof%unimportant (cases "S = {}")
   case True
   then show ?thesis
     using KS homeomorphism_ident that by fastforce
@@ -7875,7 +7876,7 @@
 qed
 
 
-subsubsection\<open>The theorem \<open>homeomorphism_grouping_points_exists\<close>\<close>
+subsubsection%unimportant\<open>The theorem \<open>homeomorphism_grouping_points_exists\<close>\<close>
 
 lemma homeomorphism_grouping_point_1:
   fixes a::real and c::real
@@ -8112,12 +8113,12 @@
   qed
 qed
 
-proposition homeomorphism_grouping_points_exists:
+proposition%important homeomorphism_grouping_points_exists:
   fixes S :: "'a::euclidean_space set"
   assumes "open U" "open S" "connected S" "U \<noteq> {}" "finite K" "K \<subseteq> S" "U \<subseteq> S" "S \<subseteq> T"
   obtains f g where "homeomorphism T T f g" "{x. (~ (f x = x \<and> g x = x))} \<subseteq> S"
                     "bounded {x. (~ (f x = x \<and> g x = x))}" "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U"
-proof (cases "2 \<le> DIM('a)")
+proof%unimportant (cases "2 \<le> DIM('a)")
   case True
   have TS: "T \<subseteq> affine hull S"
     using affine_hull_open assms by blast
@@ -8401,13 +8402,13 @@
   qed
 qed
 
-proposition nullhomotopic_from_sphere_extension:
+proposition%important nullhomotopic_from_sphere_extension:
   fixes f :: "'M::euclidean_space \<Rightarrow> 'a::real_normed_vector"
   shows  "(\<exists>c. homotopic_with (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)) \<longleftrightarrow>
           (\<exists>g. continuous_on (cball a r) g \<and> g ` (cball a r) \<subseteq> S \<and>
                (\<forall>x \<in> sphere a r. g x = f x))"
          (is "?lhs = ?rhs")
-proof (cases r "0::real" rule: linorder_cases)
+proof%unimportant (cases r "0::real" rule: linorder_cases)
   case less
   then show ?thesis by simp
 next
diff -r 9c31678d2139 -r 0acdcd8f4ba1 src/HOL/Analysis/Product_Vector.thy
--- a/src/HOL/Analysis/Product_Vector.thy	Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Product_Vector.thy	Fri Apr 06 17:34:50 2018 +0200
@@ -12,7 +12,7 @@
 
 subsection \<open>Product is a real vector space\<close>
 
-instantiation prod :: (real_vector, real_vector) real_vector
+instantiation%important prod :: (real_vector, real_vector) real_vector
 begin
 
 definition scaleR_prod_def:
@@ -46,10 +46,10 @@
 
 (* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
 
-instantiation prod :: (metric_space, metric_space) dist
+instantiation%important prod :: (metric_space, metric_space) dist
 begin
 
-definition dist_prod_def[code del]:
+definition%important dist_prod_def[code del]:
   "dist x y = sqrt ((dist (fst x) (fst y))\<^sup>2 + (dist (snd x) (snd y))\<^sup>2)"
 
 instance ..
@@ -68,7 +68,7 @@
 
 declare uniformity_Abort[where 'a="'a :: metric_space \<times> 'b :: metric_space", code]
 
-instantiation prod :: (metric_space, metric_space) metric_space
+instantiation%important prod :: (metric_space, metric_space) metric_space
 begin
 
 lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<^sup>2 + (dist b d)\<^sup>2)"
@@ -186,8 +186,8 @@
 
 subsection \<open>Product is a complete metric space\<close>
 
-instance prod :: (complete_space, complete_space) complete_space
-proof
+instance%important prod :: (complete_space, complete_space) complete_space
+proof%unimportant
   fix X :: "nat \<Rightarrow> 'a \<times> 'b" assume "Cauchy X"
   have 1: "(\<lambda>n. fst (X n)) \<longlonglongrightarrow> lim (\<lambda>n. fst (X n))"
     using Cauchy_fst [OF \<open>Cauchy X\<close>]
@@ -203,7 +203,7 @@
 
 subsection \<open>Product is a normed vector space\<close>
 
-instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector
+instantiation%important prod :: (real_normed_vector, real_normed_vector) real_normed_vector
 begin
 
 definition norm_prod_def[code del]:
@@ -245,13 +245,13 @@
 
 instance prod :: (banach, banach) banach ..
 
-subsubsection \<open>Pair operations are linear\<close>
+subsubsection%unimportant \<open>Pair operations are linear\<close>
 
-lemma bounded_linear_fst: "bounded_linear fst"
+lemma%important bounded_linear_fst: "bounded_linear fst"
   using fst_add fst_scaleR
   by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
 
-lemma bounded_linear_snd: "bounded_linear snd"
+lemma%important bounded_linear_snd: "bounded_linear snd"
   using snd_add snd_scaleR
   by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
 
@@ -285,12 +285,12 @@
   then show "\<exists>K. \<forall>x. norm (f x, g x) \<le> norm x * K" ..
 qed
 
-subsubsection \<open>Frechet derivatives involving pairs\<close>
+subsubsection%unimportant \<open>Frechet derivatives involving pairs\<close>
 
-lemma has_derivative_Pair [derivative_intros]:
+lemma%important has_derivative_Pair [derivative_intros]:
   assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
   shows "((\<lambda>x. (f x, g x)) has_derivative (\<lambda>h. (f' h, g' h))) (at x within s)"
-proof (rule has_derivativeI_sandwich[of 1])
+proof%unimportant (rule has_derivativeI_sandwich[of 1])
   show "bounded_linear (\<lambda>h. (f' h, g' h))"
     using f g by (intro bounded_linear_Pair has_derivative_bounded_linear)
   let ?Rf = "\<lambda>y. f y - f x - f' (y - x)"
@@ -319,7 +319,7 @@
   unfolding split_beta' .
 
 
-subsubsection \<open>Vector derivatives involving pairs\<close>
+subsubsection%unimportant \<open>Vector derivatives involving pairs\<close>
 
 lemma has_vector_derivative_Pair[derivative_intros]:
   assumes "(f has_vector_derivative f') (at x within s)"
@@ -331,7 +331,7 @@
 
 subsection \<open>Product is an inner product space\<close>
 
-instantiation prod :: (real_inner, real_inner) real_inner
+instantiation%important prod :: (real_inner, real_inner) real_inner
 begin
 
 definition inner_prod_def:
diff -r 9c31678d2139 -r 0acdcd8f4ba1 src/HOL/Analysis/Sigma_Algebra.thy
--- a/src/HOL/Analysis/Sigma_Algebra.thy	Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Fri Apr 06 17:34:50 2018 +0200
@@ -5,7 +5,7 @@
     translated by Lawrence Paulson.
 *)
 
-section \<open>Describing measurable sets\<close>
+section \<open>Sigma Algebra\<close>
 
 theory Sigma_Algebra
 imports
@@ -27,7 +27,7 @@
 
 subsection \<open>Families of sets\<close>
 
-locale subset_class =
+locale%important subset_class =
   fixes \<Omega> :: "'a set" and M :: "'a set set"
   assumes space_closed: "M \<subseteq> Pow \<Omega>"
 
@@ -36,7 +36,7 @@
 
 subsubsection \<open>Semiring of sets\<close>
 
-locale semiring_of_sets = subset_class +
+locale%important semiring_of_sets = subset_class +
   assumes empty_sets[iff]: "{} \<in> M"
   assumes Int[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b \<in> M"
   assumes Diff_cover:
@@ -71,7 +71,9 @@
   with assms show ?thesis by auto
 qed
 
-locale ring_of_sets = semiring_of_sets +
+subsubsection \<open>Ring of sets\<close>
+
+locale%important ring_of_sets = semiring_of_sets +
   assumes Un [intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M"
 
 lemma (in ring_of_sets) finite_Union [intro]:
@@ -135,20 +137,22 @@
   with assms show ?thesis by auto
 qed
 
-locale algebra = ring_of_sets +
+subsubsection \<open>Algebra of sets\<close>
+
+locale%important algebra = ring_of_sets +
   assumes top [iff]: "\<Omega> \<in> M"
 
 lemma (in algebra) compl_sets [intro]:
   "a \<in> M \<Longrightarrow> \<Omega> - a \<in> M"
   by auto
 
-lemma algebra_iff_Un:
+lemma%important algebra_iff_Un:
   "algebra \<Omega> M \<longleftrightarrow>
     M \<subseteq> Pow \<Omega> \<and>
     {} \<in> M \<and>
     (\<forall>a \<in> M. \<Omega> - a \<in> M) \<and>
     (\<forall>a \<in> M. \<forall> b \<in> M. a \<union> b \<in> M)" (is "_ \<longleftrightarrow> ?Un")
-proof
+proof%unimportant
   assume "algebra \<Omega> M"
   then interpret algebra \<Omega> M .
   show ?Un using sets_into_space by auto
@@ -169,12 +173,12 @@
   show "algebra \<Omega> M" proof qed fact
 qed
 
-lemma algebra_iff_Int:
+lemma%important algebra_iff_Int:
      "algebra \<Omega> M \<longleftrightarrow>
        M \<subseteq> Pow \<Omega> & {} \<in> M &
        (\<forall>a \<in> M. \<Omega> - a \<in> M) &
        (\<forall>a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)" (is "_ \<longleftrightarrow> ?Int")
-proof
+proof%unimportant
   assume "algebra \<Omega> M"
   then interpret algebra \<Omega> M .
   show ?Int using sets_into_space by auto
@@ -214,7 +218,7 @@
   "X \<subseteq> S \<Longrightarrow> algebra S { {}, X, S - X, S }"
   by (auto simp: algebra_iff_Int)
 
-subsubsection \<open>Restricted algebras\<close>
+subsubsection%unimportant \<open>Restricted algebras\<close>
 
 abbreviation (in algebra)
   "restricted_space A \<equiv> ((\<inter>) A) ` M"
@@ -225,7 +229,7 @@
 
 subsubsection \<open>Sigma Algebras\<close>
 
-locale sigma_algebra = algebra +
+locale%important sigma_algebra = algebra +
   assumes countable_nat_UN [intro]: "\<And>A. range A \<subseteq> M \<Longrightarrow> (\<Union>i::nat. A i) \<in> M"
 
 lemma (in algebra) is_sigma_algebra:
@@ -423,7 +427,7 @@
   shows "sigma_algebra S { {}, X, S - X, S }"
   using algebra.is_sigma_algebra[OF algebra_single_set[OF \<open>X \<subseteq> S\<close>]] by simp
 
-subsubsection \<open>Binary Unions\<close>
+subsubsection%unimportant \<open>Binary Unions\<close>
 
 definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
   where "binary a b =  (\<lambda>x. b)(0 := a)"
@@ -447,10 +451,10 @@
 
 subsubsection \<open>Initial Sigma Algebra\<close>
 
-text \<open>Sigma algebras can naturally be created as the closure of any set of
+text%important \<open>Sigma algebras can naturally be created as the closure of any set of
   M with regard to the properties just postulated.\<close>
 
-inductive_set sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
+inductive_set%important sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
   for sp :: "'a set" and A :: "'a set set"
   where
     Basic[intro, simp]: "a \<in> A \<Longrightarrow> a \<in> sigma_sets sp A"
@@ -796,7 +800,7 @@
   thus "(\<Union>i::nat. A i) \<in> M" by (simp add: UN_disjointed_eq)
 qed
 
-subsubsection \<open>Ring generated by a semiring\<close>
+subsubsection%unimportant \<open>Ring generated by a semiring\<close>
 
 definition (in semiring_of_sets)
   "generated_ring = { \<Union>C | C. C \<subseteq> M \<and> finite C \<and> disjoint C }"
@@ -927,7 +931,7 @@
     by (blast intro!: sigma_sets_mono elim: generated_ringE)
 qed (auto intro!: generated_ringI_Basic sigma_sets_mono)
 
-subsubsection \<open>A Two-Element Series\<close>
+subsubsection%unimportant \<open>A Two-Element Series\<close>
 
 definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set"
   where "binaryset A B = (\<lambda>x. {})(0 := A, Suc 0 := B)"
@@ -943,7 +947,7 @@
 
 subsubsection \<open>Closed CDI\<close>
 
-definition closed_cdi where
+definition%important closed_cdi where
   "closed_cdi \<Omega> M \<longleftrightarrow>
    M \<subseteq> Pow \<Omega> &
    (\<forall>s \<in> M. \<Omega> - s \<in> M) &
@@ -1177,7 +1181,7 @@
 
 subsubsection \<open>Dynkin systems\<close>
 
-locale dynkin_system = subset_class +
+locale%important dynkin_system = subset_class +
   assumes space: "\<Omega> \<in> M"
     and   compl[intro!]: "\<And>A. A \<in> M \<Longrightarrow> \<Omega> - A \<in> M"
     and   UN[intro!]: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> M
@@ -1239,7 +1243,7 @@
 
 subsubsection "Intersection sets systems"
 
-definition "Int_stable M \<longleftrightarrow> (\<forall> a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)"
+definition%important "Int_stable M \<longleftrightarrow> (\<forall> a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)"
 
 lemma (in algebra) Int_stable: "Int_stable M"
   unfolding Int_stable_def by auto
@@ -1279,7 +1283,7 @@
 
 subsubsection "Smallest Dynkin systems"
 
-definition dynkin where
+definition%important dynkin where
   "dynkin \<Omega> M =  (\<Inter>{D. dynkin_system \<Omega> D \<and> M \<subseteq> D})"
 
 lemma dynkin_system_dynkin:
@@ -1426,10 +1430,10 @@
 
 subsubsection \<open>Induction rule for intersection-stable generators\<close>
 
-text \<open>The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras
+text%important \<open>The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras
 generated by a generator closed under intersection.\<close>
 
-lemma sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
+lemma%important sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
   assumes "Int_stable G"
     and closed: "G \<subseteq> Pow \<Omega>"
     and A: "A \<in> sigma_sets \<Omega> G"
@@ -1438,7 +1442,7 @@
     and compl: "\<And>A. A \<in> sigma_sets \<Omega> G \<Longrightarrow> P A \<Longrightarrow> P (\<Omega> - A)"
     and union: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sigma_sets \<Omega> G \<Longrightarrow> (\<And>i. P (A i)) \<Longrightarrow> P (\<Union>i::nat. A i)"
   shows "P A"
-proof -
+proof%unimportant -
   let ?D = "{ A \<in> sigma_sets \<Omega> G. P A }"
   interpret sigma_algebra \<Omega> "sigma_sets \<Omega> G"
     using closed by (rule sigma_algebra_sigma_sets)
@@ -1452,34 +1456,34 @@
 
 subsection \<open>Measure type\<close>
 
-definition positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
+definition%important positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
   "positive M \<mu> \<longleftrightarrow> \<mu> {} = 0"
 
-definition countably_additive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
+definition%important countably_additive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
   "countably_additive M f \<longleftrightarrow> (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow>
     (\<Sum>i. f (A i)) = f (\<Union>i. A i))"
 
-definition measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
+definition%important measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
   "measure_space \<Omega> A \<mu> \<longleftrightarrow> sigma_algebra \<Omega> A \<and> positive A \<mu> \<and> countably_additive A \<mu>"
 
-typedef 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
-proof
+typedef%important 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
+proof%unimportant
   have "sigma_algebra UNIV {{}, UNIV}"
     by (auto simp: sigma_algebra_iff2)
   then show "(UNIV, {{}, UNIV}, \<lambda>A. 0) \<in> {(\<Omega>, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu>} "
     by (auto simp: measure_space_def positive_def countably_additive_def)
 qed
 
-definition space :: "'a measure \<Rightarrow> 'a set" where
+definition%important space :: "'a measure \<Rightarrow> 'a set" where
   "space M = fst (Rep_measure M)"
 
-definition sets :: "'a measure \<Rightarrow> 'a set set" where
+definition%important sets :: "'a measure \<Rightarrow> 'a set set" where
   "sets M = fst (snd (Rep_measure M))"
 
-definition emeasure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal" where
+definition%important emeasure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal" where
   "emeasure M = snd (snd (Rep_measure M))"
 
-definition measure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> real" where
+definition%important measure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> real" where
   "measure M A = enn2real (emeasure M A)"
 
 declare [[coercion sets]]
@@ -1494,7 +1498,7 @@
 interpretation sets: sigma_algebra "space M" "sets M" for M :: "'a measure"
   using measure_space[of M] by (auto simp: measure_space_def)
 
-definition measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where
+definition%important measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where
   "measure_of \<Omega> A \<mu> = Abs_measure (\<Omega>, if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>},
     \<lambda>a. if a \<in> sigma_sets \<Omega> A \<and> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> then \<mu> a else 0)"
 
@@ -1629,12 +1633,12 @@
 
 subsubsection \<open>Constructing simple @{typ "'a measure"}\<close>
 
-lemma emeasure_measure_of:
+lemma%important emeasure_measure_of:
   assumes M: "M = measure_of \<Omega> A \<mu>"
   assumes ms: "A \<subseteq> Pow \<Omega>" "positive (sets M) \<mu>" "countably_additive (sets M) \<mu>"
   assumes X: "X \<in> sets M"
   shows "emeasure M X = \<mu> X"
-proof -
+proof%unimportant -
   interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" by (rule sigma_algebra_sigma_sets) fact
   have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>"
     using ms M by (simp add: measure_space_def sigma_algebra_sigma_sets)
@@ -1711,7 +1715,7 @@
 
 subsubsection \<open>Measurable functions\<close>
 
-definition measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>M" 60) where
+definition%important measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>M" 60) where
   "measurable A B = {f \<in> space A \<rightarrow> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
 
 lemma measurableI:
@@ -1873,7 +1877,7 @@
 
 subsubsection \<open>Counting space\<close>
 
-definition count_space :: "'a set \<Rightarrow> 'a measure" where
+definition%important count_space :: "'a set \<Rightarrow> 'a measure" where
   "count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then of_nat (card A) else \<infinity>)"
 
 lemma
@@ -1949,7 +1953,7 @@
   "space N = {} \<Longrightarrow> f \<in> measurable M N \<longleftrightarrow> space M = {}"
   by (auto simp add: measurable_def Pi_iff)
 
-subsubsection \<open>Extend measure\<close>
+subsubsection%unimportant \<open>Extend measure\<close>
 
 definition "extend_measure \<Omega> I G \<mu> =
   (if (\<exists>\<mu>'. (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>') \<and> \<not> (\<forall>i\<in>I. \<mu> i = 0)
@@ -2011,7 +2015,7 @@
 
 subsection \<open>The smallest $\sigma$-algebra regarding a function\<close>
 
-definition
+definition%important
   "vimage_algebra X f M = sigma X {f -` A \<inter> X | A. A \<in> sets M}"
 
 lemma space_vimage_algebra[simp]: "space (vimage_algebra X f M) = X"
diff -r 9c31678d2139 -r 0acdcd8f4ba1 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Starlike.thy	Fri Apr 06 17:34:50 2018 +0200
@@ -15,7 +15,7 @@
 
 subsection \<open>Midpoint\<close>
 
-definition midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
+definition%important midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
   where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"
 
 lemma midpoint_idem [simp]: "midpoint x x = x"
@@ -94,10 +94,10 @@
 
 subsection \<open>Line segments\<close>
 
-definition closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
+definition%important closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
   where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
 
-definition open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
+definition%important open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
   "open_segment a b \<equiv> closed_segment a b - {a,b}"
 
 lemmas segment = open_segment_def closed_segment_def
@@ -599,7 +599,7 @@
 
 subsection\<open>Starlike sets\<close>
 
-definition "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
+definition%important "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
 
 lemma starlike_UNIV [simp]: "starlike UNIV"
   by (simp add: starlike_def)
@@ -662,7 +662,7 @@
     by (meson hull_mono inf_mono subset_insertI subset_refl)
 qed
 
-subsection\<open>More results about segments\<close>
+subsection%unimportant\<open>More results about segments\<close>
 
 lemma dist_half_times2:
   fixes a :: "'a :: real_normed_vector"
@@ -884,7 +884,7 @@
 
 subsection\<open>Betweenness\<close>
 
-definition "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
+definition%important "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
 
 lemma betweenI:
   assumes "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
@@ -1055,7 +1055,7 @@
   by (auto simp: between_mem_segment closed_segment_eq_real_ivl)
 
 
-subsection \<open>Shrinking towards the interior of a convex set\<close>
+subsection%unimportant \<open>Shrinking towards the interior of a convex set\<close>
 
 lemma mem_interior_convex_shrink:
   fixes s :: "'a::euclidean_space set"
@@ -1249,7 +1249,7 @@
 qed
 
 
-subsection \<open>Some obvious but surprisingly hard simplex lemmas\<close>
+subsection%unimportant \<open>Some obvious but surprisingly hard simplex lemmas\<close>
 
 lemma simplex:
   assumes "finite s"
@@ -1693,7 +1693,7 @@
 qed
 
 
-subsection \<open>Relative interior of convex set\<close>
+subsection%unimportant \<open>Relative interior of convex set\<close>
 
 lemma rel_interior_convex_nonempty_aux:
   fixes S :: "'n::euclidean_space set"
@@ -2081,7 +2081,7 @@
 
 subsection\<open>The relative frontier of a set\<close>
 
-definition "rel_frontier S = closure S - rel_interior S"
+definition%important "rel_frontier S = closure S - rel_interior S"
 
 lemma rel_frontier_empty [simp]: "rel_frontier {} = {}"
   by (simp add: rel_frontier_def)
@@ -2460,7 +2460,7 @@
 qed
 
 
-subsubsection \<open>Relative interior and closure under common operations\<close>
+subsubsection%unimportant \<open>Relative interior and closure under common operations\<close>
 
 lemma rel_interior_inter_aux: "\<Inter>{rel_interior S |S. S \<in> I} \<subseteq> \<Inter>I"
 proof -
@@ -3150,7 +3150,7 @@
     by (force simp: rel_frontier_def rel_interior_Times assms closure_Times)
 
 
-subsubsection \<open>Relative interior of convex cone\<close>
+subsubsection%unimportant \<open>Relative interior of convex cone\<close>
 
 lemma cone_rel_interior:
   fixes S :: "'m::euclidean_space set"
@@ -3423,7 +3423,7 @@
 qed
 
 
-subsection \<open>Convexity on direct sums\<close>
+subsection%unimportant \<open>Convexity on direct sums\<close>
 
 lemma closure_sum:
   fixes S T :: "'a::real_normed_vector set"
@@ -3794,7 +3794,7 @@
     using \<open>y < x\<close> by (simp add: field_simps)
 qed simp
 
-subsection\<open>Explicit formulas for interior and relative interior of convex hull\<close>
+subsection%unimportant\<open>Explicit formulas for interior and relative interior of convex hull\<close>
 
 lemma at_within_cbox_finite:
   assumes "x \<in> box a b" "x \<notin> S" "finite S"
@@ -4157,7 +4157,7 @@
     by (metis Diff_cancel convex_hull_singleton insert_absorb2 open_segment_def segment_convex_hull)
 qed
 
-subsection\<open>Similar results for closure and (relative or absolute) frontier.\<close>
+subsection%unimportant\<open>Similar results for closure and (relative or absolute) frontier.\<close>
 
 lemma closure_convex_hull [simp]:
   fixes s :: "'a::euclidean_space set"
@@ -4315,7 +4315,7 @@
 
 subsection \<open>Coplanarity, and collinearity in terms of affine hull\<close>
 
-definition coplanar  where
+definition%important coplanar  where
    "coplanar s \<equiv> \<exists>u v w. s \<subseteq> affine hull {u,v,w}"
 
 lemma collinear_affine_hull:
@@ -4767,7 +4767,7 @@
 
 subsection\<open>The infimum of the distance between two sets\<close>
 
-definition setdist :: "'a::metric_space set \<Rightarrow> 'a set \<Rightarrow> real" where
+definition%important setdist :: "'a::metric_space set \<Rightarrow> 'a set \<Rightarrow> real" where
   "setdist s t \<equiv>
        (if s = {} \<or> t = {} then 0
         else Inf {dist x y| x y. x \<in> s \<and> y \<in> t})"
@@ -5003,7 +5003,7 @@
          \<Longrightarrow> setdist {x} S > 0"
   using less_eq_real_def setdist_eq_0_closedin by fastforce
 
-subsection\<open>Basic lemmas about hyperplanes and halfspaces\<close>
+subsection%unimportant\<open>Basic lemmas about hyperplanes and halfspaces\<close>
 
 lemma hyperplane_eq_Ex:
   assumes "a \<noteq> 0" obtains x where "a \<bullet> x = b"
@@ -5056,7 +5056,7 @@
 using halfspace_eq_empty_le [of "-a" "-b"]
 by simp
 
-subsection\<open>Use set distance for an easy proof of separation properties\<close>
+subsection%unimportant\<open>Use set distance for an easy proof of separation properties\<close>
 
 proposition separation_closures:
   fixes S :: "'a::euclidean_space set"
@@ -5150,12 +5150,12 @@
 
 subsection\<open>Connectedness of the intersection of a chain\<close>
 
-proposition connected_chain:
+proposition%important connected_chain:
   fixes \<F> :: "'a :: euclidean_space set set"
   assumes cc: "\<And>S. S \<in> \<F> \<Longrightarrow> compact S \<and> connected S"
       and linear: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
   shows "connected(\<Inter>\<F>)"
-proof (cases "\<F> = {}")
+proof%unimportant (cases "\<F> = {}")
   case True then show ?thesis
     by auto
 next
@@ -5299,13 +5299,13 @@
       by (meson le_max_iff_disj)
 qed
 
-proposition proper_map:
+proposition%important proper_map:
   fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
   assumes "closedin (subtopology euclidean S) K"
       and com: "\<And>U. \<lbrakk>U \<subseteq> T; compact U\<rbrakk> \<Longrightarrow> compact (S \<inter> f -` U)"
       and "f ` S \<subseteq> T"
     shows "closedin (subtopology euclidean T) (f ` K)"
-proof -
+proof%unimportant -
   have "K \<subseteq> S"
     using assms closedin_imp_subset by metis
   obtain C where "closed C" and Keq: "K = S \<inter> C"
@@ -5387,7 +5387,7 @@
     by (simp add: continuous_on_closed * closedin_imp_subset)
 qed
 
-subsection\<open>Trivial fact: convexity equals connectedness for collinear sets\<close>
+subsection%unimportant\<open>Trivial fact: convexity equals connectedness for collinear sets\<close>
 
 lemma convex_connected_collinear:
   fixes S :: "'a::euclidean_space set"
@@ -5605,7 +5605,7 @@
     by (simp add: clo closedin_closed_Int)
 qed
 
-subsubsection\<open>Representing affine hull as a finite intersection of hyperplanes\<close>
+subsubsection%unimportant\<open>Representing affine hull as a finite intersection of hyperplanes\<close>
 
 proposition affine_hull_convex_Int_nonempty_interior:
   fixes S :: "'a::real_normed_vector set"
@@ -5778,7 +5778,7 @@
         (if a = 0 \<and> r > 0 then -1 else DIM('a))"
 using aff_dim_halfspace_le [of "-a" "-r"] by simp
 
-subsection\<open>Properties of special hyperplanes\<close>
+subsection%unimportant\<open>Properties of special hyperplanes\<close>
 
 lemma subspace_hyperplane: "subspace {x. a \<bullet> x = 0}"
   by (simp add: subspace_def inner_right_distrib)
@@ -5925,7 +5925,7 @@
   shows "a \<noteq> 0 \<Longrightarrow> aff_dim {x. a \<bullet> x = r} = DIM('a) - 1"
 by (metis aff_dim_eq_hyperplane affine_hull_eq affine_hyperplane)
 
-subsection\<open>Some stepping theorems\<close>
+subsection%unimportant\<open>Some stepping theorems\<close>
 
 lemma dim_empty [simp]: "dim ({} :: 'a::euclidean_space set) = 0"
   by (force intro!: dim_unique)
@@ -6092,7 +6092,7 @@
     by (metis One_nat_def \<open>a \<noteq> 0\<close> affine_bounded_eq_lowdim affine_hyperplane bounded_hyperplane_eq_trivial_0)
 qed
 
-subsection\<open>General case without assuming closure and getting non-strict separation\<close>
+subsection%unimportant\<open>General case without assuming closure and getting non-strict separation\<close>
 
 proposition separating_hyperplane_closed_point_inset:
   fixes S :: "'a::euclidean_space set"
@@ -6280,7 +6280,7 @@
 by (metis assms convex_closure convex_rel_interior_closure)
 
 
-subsection\<open> Some results on decomposing convex hulls: intersections, simplicial subdivision\<close>
+subsection%unimportant\<open> Some results on decomposing convex hulls: intersections, simplicial subdivision\<close>
 
 lemma
   fixes s :: "'a::euclidean_space set"
@@ -6636,7 +6636,7 @@
   qed
 qed
 
-subsection\<open>Misc results about span\<close>
+subsection%unimportant\<open>Misc results about span\<close>
 
 lemma eq_span_insert_eq:
   assumes "(x - y) \<in> span S"
@@ -7026,11 +7026,11 @@
 apply (simp add: x)
 done
 
-proposition Gram_Schmidt_step:
+proposition%important Gram_Schmidt_step:
   fixes S :: "'a::euclidean_space set"
   assumes S: "pairwise orthogonal S" and x: "x \<in> span S"
     shows "orthogonal x (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b))"
-proof -
+proof%unimportant -
   have "finite S"
     by (simp add: S pairwise_orthogonal_imp_finite)
   have "orthogonal (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)) x"
@@ -7087,11 +7087,11 @@
 qed
 
 
-proposition orthogonal_extension:
+proposition%important orthogonal_extension:
   fixes S :: "'a::euclidean_space set"
   assumes S: "pairwise orthogonal S"
   obtains U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
-proof -
+proof%unimportant -
   obtain B where "finite B" "span B = span T"
     using basis_subspace_exists [of "span T"] subspace_span by auto
   with orthogonal_extension_aux [of B S]
@@ -7149,13 +7149,13 @@
     done
 qed
 
-proposition orthonormal_basis_subspace:
+proposition%important orthonormal_basis_subspace:
   fixes S :: "'a :: euclidean_space set"
   assumes "subspace S"
   obtains B where "B \<subseteq> S" "pairwise orthogonal B"
               and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
               and "independent B" "card B = dim S" "span B = S"
-proof -
+proof%unimportant -
   obtain B where "0 \<notin> B" "B \<subseteq> S"
              and orth: "pairwise orthogonal B"
              and "independent B" "card B = dim S" "span B = S"
@@ -7186,11 +7186,11 @@
 qed
 
 
-proposition orthogonal_to_subspace_exists_gen:
+proposition%important orthogonal_to_subspace_exists_gen:
   fixes S :: "'a :: euclidean_space set"
   assumes "span S \<subset> span T"
   obtains x where "x \<noteq> 0" "x \<in> span T" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
-proof -
+proof%unimportant -
   obtain B where "B \<subseteq> span S" and orthB: "pairwise orthogonal B"
              and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
              and "independent B" "card B = dim S" "span B = span S"
@@ -7249,10 +7249,10 @@
     by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_clauses(1) that)
 qed
 
-proposition orthogonal_subspace_decomp_exists:
+proposition%important orthogonal_subspace_decomp_exists:
   fixes S :: "'a :: euclidean_space set"
   obtains y z where "y \<in> span S" "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w" "x = y + z"
-proof -
+proof%unimportant -
   obtain T where "0 \<notin> T" "T \<subseteq> span S" "pairwise orthogonal T" "independent T" "card T = dim (span S)" "span T = span S"
     using orthogonal_basis_subspace subspace_span by blast
   let ?a = "\<Sum>b\<in>T. (b \<bullet> x / (b \<bullet> b)) *\<^sub>R b"
@@ -7341,11 +7341,11 @@
   qed
 qed
 
-proposition dim_orthogonal_sum:
+proposition%important dim_orthogonal_sum:
   fixes A :: "'a::euclidean_space set"
   assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
     shows "dim(A \<union> B) = dim A + dim B"
-proof -
+proof%unimportant -
   have 1: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
     by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms)
   have "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
@@ -7472,10 +7472,10 @@
 
 subsection\<open>Lower-dimensional affine subsets are nowhere dense.\<close>
 
-proposition dense_complement_subspace:
+proposition%important dense_complement_subspace:
   fixes S :: "'a :: euclidean_space set"
   assumes dim_less: "dim T < dim S" and "subspace S" shows "closure(S - T) = S"
-proof -
+proof%unimportant -
   have "closure(S - U) = S" if "dim U < dim S" "U \<subseteq> S" for U
   proof -
     have "span U \<subset> span S"
@@ -7583,7 +7583,7 @@
   by (simp add: assms dense_complement_convex)
 
 
-subsection\<open>Parallel slices, etc.\<close>
+subsection%unimportant\<open>Parallel slices, etc.\<close>
 
 text\<open> If we take a slice out of a set, we can do it perpendicularly,
   with the normal vector to the slice parallel to the affine hull.\<close>
@@ -7811,7 +7811,7 @@
 
 subsection\<open>Several Variants of Paracompactness\<close>
 
-proposition paracompact:
+proposition%important paracompact:
   fixes S :: "'a :: euclidean_space set"
   assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
   obtains \<C>' where "S \<subseteq> \<Union> \<C>'"
@@ -7819,7 +7819,7 @@
                and "\<And>x. x \<in> S
                        \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and>
                                finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
-proof (cases "S = {}")
+proof%unimportant (cases "S = {}")
   case True with that show ?thesis by blast
 next
   case False
@@ -7955,7 +7955,7 @@
 using paracompact_closedin [of UNIV S \<C>] assms by auto
 
   
-subsection\<open>Closed-graph characterization of continuity\<close>
+subsection%unimportant\<open>Closed-graph characterization of continuity\<close>
 
 lemma continuous_closed_graph_gen:
   fixes T :: "'b::real_normed_vector set"
@@ -8026,7 +8026,7 @@
     by (rule continuous_on_Un_local_open [OF opS opT])
 qed
   
-subsection\<open>The union of two collinear segments is another segment\<close>
+subsection%unimportant\<open>The union of two collinear segments is another segment\<close>
 
 proposition in_convex_hull_exchange:
   fixes a :: "'a::euclidean_space"
@@ -8204,14 +8204,14 @@
 
 subsection\<open>Covering an open set by a countable chain of compact sets\<close>
   
-proposition open_Union_compact_subsets:
+proposition%important open_Union_compact_subsets:
   fixes S :: "'a::euclidean_space set"
   assumes "open S"
   obtains C where "\<And>n. compact(C n)" "\<And>n. C n \<subseteq> S"
                   "\<And>n. C n \<subseteq> interior(C(Suc n))"
                   "\<Union>(range C) = S"
                   "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. K \<subseteq> (C n)"
-proof (cases "S = {}")
+proof%unimportant (cases "S = {}")
   case True
   then show ?thesis
     by (rule_tac C = "\<lambda>n. {}" in that) auto
diff -r 9c31678d2139 -r 0acdcd8f4ba1 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Apr 06 17:34:50 2018 +0200
@@ -131,7 +131,7 @@
 context topological_space
 begin
 
-definition "topological_basis B \<longleftrightarrow>
+definition%important "topological_basis B \<longleftrightarrow>
   (\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))"
 
 lemma topological_basis:
@@ -257,7 +257,7 @@
 
 subsection \<open>Countable Basis\<close>
 
-locale countable_basis =
+locale%important countable_basis =
   fixes B :: "'a::topological_space set set"
   assumes is_basis: "topological_basis B"
     and countable_basis: "countable B"
@@ -578,19 +578,19 @@
   then show ?thesis using B(1) by auto
 qed
 
-subsection \<open>Polish spaces\<close>
+subsection%important \<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>
 
-class polish_space = complete_space + second_countable_topology
+class%important polish_space = complete_space + second_countable_topology
 
 subsection \<open>General notion of a topology as a value\<close>
 
-definition "istopology L \<longleftrightarrow>
+definition%important "istopology L \<longleftrightarrow>
   L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union>K))"
 
-typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
+typedef%important 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
   morphisms "openin" "topology"
   unfolding istopology_def by blast
 
@@ -620,7 +620,7 @@
 
 subsubsection \<open>Main properties of open sets\<close>
 
-lemma openin_clauses:
+lemma%important openin_clauses:
   fixes U :: "'a topology"
   shows
     "openin U {}"
@@ -683,7 +683,7 @@
 
 subsubsection \<open>Closed sets\<close>
 
-definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
+definition%important "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
 
 lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U"
   by (metis closedin_def)
@@ -755,7 +755,7 @@
 
 subsubsection \<open>Subspace topology\<close>
 
-definition "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
+definition%important "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
 
 lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
   (is "istopology ?L")
@@ -870,7 +870,7 @@
 
 subsubsection \<open>The standard Euclidean topology\<close>
 
-definition euclidean :: "'a::topological_space topology"
+definition%important euclidean :: "'a::topological_space topology"
   where "euclidean = topology open"
 
 lemma open_openin: "open S \<longleftrightarrow> openin euclidean S"
@@ -1054,13 +1054,13 @@
 
 subsection \<open>Open and closed balls\<close>
 
-definition ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
+definition%important ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
   where "ball x e = {y. dist x y < e}"
 
-definition cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
+definition%important cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
   where "cball x e = {y. dist x y \<le> e}"
 
-definition sphere :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
+definition%important sphere :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
   where "sphere x e = {y. dist x y = e}"
 
 lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e"
@@ -1327,11 +1327,11 @@
 corollary Zero_neq_One[iff]: "0 \<noteq> One"
   by (metis One_non_0)
 
-definition (in euclidean_space) eucl_less (infix "<e" 50)
+definition%important (in euclidean_space) eucl_less (infix "<e" 50)
   where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
 
-definition box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
-definition "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}"
+definition%important box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
+definition%important "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}"
 
 lemma box_def: "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}"
   and in_box_eucl_less: "x \<in> box a b \<longleftrightarrow> a <e x \<and> x <e b"
@@ -1873,9 +1873,9 @@
     by (auto simp: box_def inner_sum_left inner_Basis sum.If_cases)
 qed
 
-text \<open>Intervals in general, including infinite and mixtures of open and closed.\<close>
-
-definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
+subsection \<open>Intervals in general, including infinite and mixtures of open and closed.\<close>
+
+definition%important "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
   (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
 
 lemma is_interval_1:
@@ -2053,7 +2053,7 @@
 
 subsection \<open>Limit points\<close>
 
-definition (in topological_space) islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool"  (infixr "islimpt" 60)
+definition%important (in topological_space) islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool"  (infixr "islimpt" 60)
   where "x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))"
 
 lemma islimptI:
@@ -2191,7 +2191,7 @@
 
 subsection \<open>Interior of a Set\<close>
 
-definition "interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
+definition%important "interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
 
 lemma interiorI [intro?]:
   assumes "open T" and "x \<in> T" and "T \<subseteq> S"
@@ -2359,7 +2359,7 @@
 
 subsection \<open>Closure of a Set\<close>
 
-definition "closure S = S \<union> {x | x. x islimpt S}"
+definition%important "closure S = S \<union> {x | x. x islimpt S}"
 
 lemma interior_closure: "interior S = - (closure (- S))"
   by (auto simp: interior_def closure_def islimpt_def)
@@ -2635,7 +2635,7 @@
 
 subsection \<open>Frontier (also known as boundary)\<close>
 
-definition "frontier S = closure S - interior S"
+definition%important "frontier S = closure S - interior S"
 
 lemma frontier_closed [iff]: "closed (frontier S)"
   by (simp add: frontier_def closed_Diff)
@@ -2726,7 +2726,7 @@
 qed
 
 
-subsection \<open>Filters and the ``eventually true'' quantifier\<close>
+subsection%unimportant \<open>Filters and the ``eventually true'' quantifier\<close>
 
 definition indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter"  (infixr "indirection" 70)
   where "a indirection v = at a within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
@@ -2794,16 +2794,16 @@
 
 subsection \<open>Limits\<close>
 
-lemma Lim: "(f \<longlongrightarrow> l) net \<longleftrightarrow> trivial_limit net \<or> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
+lemma%important Lim: "(f \<longlongrightarrow> l) net \<longleftrightarrow> trivial_limit net \<or> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
   by (auto simp: tendsto_iff trivial_limit_eq)
 
 text \<open>Show that they yield usual definitions in the various cases.\<close>
 
-lemma Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
+lemma%important Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
     (\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> dist (f x) l < e)"
   by (auto simp: tendsto_iff eventually_at_le)
 
-lemma Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
+lemma%important Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
     (\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a  < d \<longrightarrow> dist (f x) l < e)"
   by (auto simp: tendsto_iff eventually_at)
 
@@ -2814,11 +2814,11 @@
   apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
   done
 
-lemma Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
+lemma%important Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
     (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d  \<longrightarrow> dist (f x) l < e)"
   by (auto simp: tendsto_iff eventually_at)
 
-lemma Lim_at_infinity: "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)"
+lemma%important Lim_at_infinity: "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)"
   by (auto simp: tendsto_iff eventually_at_infinity)
 
 corollary Lim_at_infinityI [intro?]:
@@ -3411,7 +3411,7 @@
 subsection \<open>Boundedness\<close>
 
   (* FIXME: This has to be unified with BSEQ!! *)
-definition (in metric_space) bounded :: "'a set \<Rightarrow> bool"
+definition%important (in metric_space) bounded :: "'a set \<Rightarrow> bool"
   where "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"
 
 lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e \<and> 0 \<le> e)"
@@ -3690,12 +3690,12 @@
 
 subsubsection \<open>Bolzano-Weierstrass property\<close>
 
-lemma heine_borel_imp_bolzano_weierstrass:
+lemma%important heine_borel_imp_bolzano_weierstrass:
   assumes "compact s"
     and "infinite t"
     and "t \<subseteq> s"
   shows "\<exists>x \<in> s. x islimpt t"
-proof (rule ccontr)
+proof%unimportant (rule ccontr)
   assume "\<not> (\<exists>x \<in> s. x islimpt t)"
   then obtain f where f: "\<forall>x\<in>s. x \<in> f x \<and> open (f x) \<and> (\<forall>y\<in>t. y \<in> f x \<longrightarrow> y = x)"
     unfolding islimpt_def
@@ -4157,7 +4157,7 @@
   with \<open>U \<inter> \<Inter>A = {}\<close> show False by auto
 qed
 
-definition "countably_compact U \<longleftrightarrow>
+definition%important "countably_compact U \<longleftrightarrow>
     (\<forall>A. countable A \<longrightarrow> (\<forall>a\<in>A. open a) \<longrightarrow> U \<subseteq> \<Union>A \<longrightarrow> (\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T))"
 
 lemma countably_compactE:
@@ -4208,9 +4208,9 @@
     unfolding C_def by (intro exI[of _ "f`T"]) fastforce
 qed
 
-lemma countably_compact_imp_compact_second_countable:
+lemma%important countably_compact_imp_compact_second_countable:
   "countably_compact U \<Longrightarrow> compact (U :: 'a :: second_countable_topology set)"
-proof (rule countably_compact_imp_compact)
+proof%unimportant (rule countably_compact_imp_compact)
   fix T and x :: 'a
   assume "open T" "x \<in> T"
   from topological_basisE[OF is_basis this] obtain b where
@@ -4225,7 +4225,7 @@
 
 subsubsection\<open>Sequential compactness\<close>
 
-definition seq_compact :: "'a::topological_space set \<Rightarrow> bool"
+definition%important seq_compact :: "'a::topological_space set \<Rightarrow> bool"
   where "seq_compact S \<longleftrightarrow>
     (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially))"
 
@@ -4486,10 +4486,10 @@
   shows "seq_compact U \<longleftrightarrow> compact U"
   using seq_compact_eq_countably_compact countably_compact_eq_compact by blast
 
-lemma bolzano_weierstrass_imp_seq_compact:
+lemma%important bolzano_weierstrass_imp_seq_compact:
   fixes s :: "'a::{t1_space, first_countable_topology} set"
   shows "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> seq_compact s"
-  by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
+  by%unimportant (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
 
 
 subsubsection\<open>Totally bounded\<close>
@@ -4497,10 +4497,10 @@
 lemma cauchy_def: "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N \<longrightarrow> dist (s m) (s n) < e)"
   unfolding Cauchy_def by metis
 
-lemma seq_compact_imp_totally_bounded:
+lemma%important seq_compact_imp_totally_bounded:
   assumes "seq_compact s"
   shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>k. ball x e)"
-proof -
+proof%unimportant -
   { fix e::real assume "e > 0" assume *: "\<And>k. finite k \<Longrightarrow> k \<subseteq> s \<Longrightarrow> \<not> s \<subseteq> (\<Union>x\<in>k. ball x e)"
     let ?Q = "\<lambda>x n r. r \<in> s \<and> (\<forall>m < (n::nat). \<not> (dist (x m) r < e))"
     have "\<exists>x. \<forall>n::nat. ?Q x n (x n)"
@@ -4529,11 +4529,11 @@
 
 subsubsection\<open>Heine-Borel theorem\<close>
 
-lemma seq_compact_imp_heine_borel:
+lemma%important seq_compact_imp_heine_borel:
   fixes s :: "'a :: metric_space set"
   assumes "seq_compact s"
   shows "compact s"
-proof -
+proof%unimportant -
   from seq_compact_imp_totally_bounded[OF \<open>seq_compact s\<close>]
   obtain f where f: "\<forall>e>0. finite (f e) \<and> f e \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>f e. ball x e)"
     unfolding choice_iff' ..
@@ -4574,22 +4574,22 @@
   qed
 qed
 
-lemma compact_eq_seq_compact_metric:
+lemma%important compact_eq_seq_compact_metric:
   "compact (s :: 'a::metric_space set) \<longleftrightarrow> seq_compact s"
   using compact_imp_seq_compact seq_compact_imp_heine_borel by blast
 
-lemma compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
+lemma%important compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
   "compact (S :: 'a::metric_space set) \<longleftrightarrow>
    (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l))"
   unfolding compact_eq_seq_compact_metric seq_compact_def by auto
 
 subsubsection \<open>Complete the chain of compactness variants\<close>
 
-lemma compact_eq_bolzano_weierstrass:
+lemma%important compact_eq_bolzano_weierstrass:
   fixes s :: "'a::metric_space set"
   shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))"
   (is "?lhs = ?rhs")
-proof
+proof%unimportant
   assume ?lhs
   then show ?rhs
     using heine_borel_imp_bolzano_weierstrass[of s] by auto
@@ -4599,7 +4599,7 @@
     unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact)
 qed
 
-lemma bolzano_weierstrass_imp_bounded:
+lemma%important bolzano_weierstrass_imp_bounded:
   "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s"
   using compact_imp_bounded unfolding compact_eq_bolzano_weierstrass .
 
@@ -4611,16 +4611,16 @@
   Heine-Borel property if every closed and bounded subset is compact.
 \<close>
 
-class heine_borel = metric_space +
+class%important heine_borel = metric_space +
   assumes bounded_imp_convergent_subsequence:
     "bounded (range f) \<Longrightarrow> \<exists>l r. strict_mono (r::nat\<Rightarrow>nat) \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
 
-lemma bounded_closed_imp_seq_compact:
+lemma%important bounded_closed_imp_seq_compact:
   fixes s::"'a::heine_borel set"
   assumes "bounded s"
     and "closed s"
   shows "seq_compact s"
-proof (unfold seq_compact_def, clarify)
+proof%unimportant (unfold seq_compact_def, clarify)
   fix f :: "nat \<Rightarrow> 'a"
   assume f: "\<forall>n. f n \<in> s"
   with \<open>bounded s\<close> have "bounded (range f)"
@@ -4690,8 +4690,8 @@
     by (metis of_nat_le_iff Int_subset_iff \<open>K \<subseteq> S\<close> real_arch_simple subset_cball subset_trans)
 qed auto
 
-instance real :: heine_borel
-proof
+instance%important real :: heine_borel
+proof%unimportant
   fix f :: "nat \<Rightarrow> real"
   assume f: "bounded (range f)"
   obtain r :: "nat \<Rightarrow> nat" where r: "strict_mono r" "monoseq (f \<circ> r)"
@@ -4771,8 +4771,8 @@
      (auto intro!: assms bounded_linear_inner_left bounded_linear_image
        simp: euclidean_representation)
 
-instance euclidean_space \<subseteq> heine_borel
-proof
+instance%important euclidean_space \<subseteq> heine_borel
+proof%unimportant
   fix f :: "nat \<Rightarrow> 'a"
   assume f: "bounded (range f)"
   then obtain l::'a and r where r: "strict_mono r"
@@ -4818,8 +4818,8 @@
   unfolding bounded_def
   by (metis (no_types, hide_lams) dist_snd_le image_iff order.trans)
 
-instance prod :: (heine_borel, heine_borel) heine_borel
-proof
+instance%important prod :: (heine_borel, heine_borel) heine_borel
+proof%unimportant
   fix f :: "nat \<Rightarrow> 'a \<times> 'b"
   assume f: "bounded (range f)"
   then have "bounded (fst ` range f)"
@@ -4845,12 +4845,12 @@
 
 subsubsection \<open>Completeness\<close>
 
-lemma (in metric_space) completeI:
+lemma%important (in metric_space) completeI:
   assumes "\<And>f. \<forall>n. f n \<in> s \<Longrightarrow> Cauchy f \<Longrightarrow> \<exists>l\<in>s. f \<longlonglongrightarrow> l"
   shows "complete s"
   using assms unfolding complete_def by fast
 
-lemma (in metric_space) completeE:
+lemma%important (in metric_space) completeE:
   assumes "complete s" and "\<forall>n. f n \<in> s" and "Cauchy f"
   obtains l where "l \<in> s" and "f \<longlonglongrightarrow> l"
   using assms unfolding complete_def by fast
@@ -4900,10 +4900,10 @@
   then show ?thesis unfolding complete_def by auto
 qed
 
-lemma compact_eq_totally_bounded:
+lemma%important compact_eq_totally_bounded:
   "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))"
     (is "_ \<longleftrightarrow> ?rhs")
-proof
+proof%unimportant
   assume assms: "?rhs"
   then obtain k where k: "\<And>e. 0 < e \<Longrightarrow> finite (k e)" "\<And>e. 0 < e \<Longrightarrow> s \<subseteq> (\<Union>x\<in>k e. ball x e)"
     by (auto simp: choice_iff')
@@ -5107,7 +5107,7 @@
 
 text\<open>Derive the epsilon-delta forms, which we often use as "definitions"\<close>
 
-lemma continuous_within_eps_delta:
+lemma%important continuous_within_eps_delta:
   "continuous (at x within s) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> s.  dist x' x < d --> dist (f x') (f x) < e)"
   unfolding continuous_within and Lim_within  by fastforce
 
@@ -5435,7 +5435,7 @@
   by (force intro: Lim_transform_within)
 
 
-subsubsection \<open>Structural rules for pointwise continuity\<close>
+subsubsection%unimportant \<open>Structural rules for pointwise continuity\<close>
 
 lemma continuous_infnorm[continuous_intros]:
   "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))"
@@ -5447,7 +5447,7 @@
   shows "continuous F (\<lambda>x. inner (f x) (g x))"
   using assms unfolding continuous_def by (rule tendsto_inner)
 
-subsubsection \<open>Structural rules for setwise continuity\<close>
+subsubsection%unimportant \<open>Structural rules for setwise continuity\<close>
 
 lemma continuous_on_infnorm[continuous_intros]:
   "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
@@ -5461,7 +5461,7 @@
   using bounded_bilinear_inner assms
   by (rule bounded_bilinear.continuous_on)
 
-subsubsection \<open>Structural rules for uniform continuity\<close>
+subsubsection%unimportant \<open>Structural rules for uniform continuity\<close>
 
 lemma uniformly_continuous_on_dist[continuous_intros]:
   fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
@@ -5653,7 +5653,7 @@
     shows "closedin (subtopology euclidean S) (S \<inter> f -` T)"
 using assms continuous_on_closed by blast
 
-subsection \<open>Half-global and completely global cases.\<close>
+subsection%unimportant \<open>Half-global and completely global cases.\<close>
 
 lemma continuous_openin_preimage_gen:
   assumes "continuous_on S f"  "open T"
@@ -5743,7 +5743,7 @@
   with \<open>x = f y\<close> show "x \<in> f ` interior S" ..
 qed
 
-subsection \<open>Topological properties of linear functions.\<close>
+subsection%unimportant \<open>Topological properties of linear functions.\<close>
 
 lemma linear_lim_0:
   assumes "bounded_linear f"
@@ -5771,7 +5771,7 @@
   "bounded_linear f \<Longrightarrow> continuous_on s f"
   using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
 
-subsection \<open>Intervals\<close>
+subsection%unimportant \<open>Intervals\<close>
 
 text \<open>Openness of halfspaces.\<close>