more tagging
authorAngeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
Thu, 17 Jan 2019 15:50:28 +0000
changeset 69678 0f4d4a13dc16
parent 69677 a06b204527e6 (current diff)
parent 69673 cc47e7e06f38 (diff)
child 69679 a8faf6f15da7
more tagging
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Cartesian_Space.thy
src/HOL/Analysis/Finite_Cartesian_Product.thy
src/HOL/Analysis/Further_Topology.thy
src/HOL/Analysis/Great_Picard.thy
src/HOL/Analysis/Homeomorphism.thy
src/HOL/Analysis/Improper_Integral.thy
src/HOL/Analysis/Interval_Integral.thy
src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Jan 16 21:27:33 2019 +0000
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Jan 17 15:50:28 2019 +0000
@@ -13,7 +13,7 @@
   "HOL-Library.FuncSet"
 begin
 
-subsection%important \<open>Finite Cartesian products, with indexing and lambdas\<close>
+subsection%unimportant \<open>Finite Cartesian products, with indexing and lambdas\<close>
 
 typedef ('a, 'b) vec = "UNIV :: ('b::finite \<Rightarrow> 'a) set"
   morphisms vec_nth vec_lambda ..
@@ -104,10 +104,10 @@
     by (auto elim!: countableE)
 qed
 
-lemma infinite_UNIV_vec:
+lemma%important infinite_UNIV_vec:
   assumes "infinite (UNIV :: 'a set)"
   shows   "infinite (UNIV :: ('a^'b) set)"
-proof (subst bij_betw_finite)
+proof%unimportant (subst bij_betw_finite)
   show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))"
     by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff)
   have "infinite (PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" (is "infinite ?A")
@@ -125,9 +125,9 @@
   finally show "infinite (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" .
 qed
 
-lemma CARD_vec [simp]:
+lemma%important CARD_vec [simp]:
   "CARD('a^'b) = CARD('a) ^ CARD('b)"
-proof (cases "finite (UNIV :: 'a set)")
+proof%unimportant (cases "finite (UNIV :: 'a set)")
   case True
   show ?thesis
   proof (subst bij_betw_same_card)
@@ -143,7 +143,7 @@
   qed
 qed (simp_all add: infinite_UNIV_vec)
 
-lemma countable_vector:
+lemma%unimportant countable_vector:
   fixes B:: "'n::finite \<Rightarrow> 'a set"
   assumes "\<And>i. countable (B i)"
   shows "countable {V. \<forall>i::'n::finite. V $ i \<in> B i}"
@@ -165,7 +165,7 @@
     by (simp add: image_comp o_def vec_nth_inverse)
 qed
 
-subsection%important \<open>Group operations and class instances\<close>
+subsection%unimportant \<open>Group operations and class instances\<close>
 
 instantiation vec :: (zero, finite) zero
 begin
@@ -230,7 +230,7 @@
   by standard (simp_all add: vec_eq_iff)
 
 
-subsection%important\<open>Basic componentwise operations on vectors\<close>
+subsection%unimportant\<open>Basic componentwise operations on vectors\<close>
 
 instantiation vec :: (times, finite) times
 begin
@@ -295,12 +295,12 @@
 
 text\<open>Also the scalar-vector multiplication.\<close>
 
-definition%important vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)
+definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)
   where "c *s x = (\<chi> i. c * (x$i))"
 
 text \<open>scalar product\<close>
 
-definition%important scalar_product :: "'a :: semiring_1 ^ 'n \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a" where
+definition scalar_product :: "'a :: semiring_1 ^ 'n \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a" where
   "scalar_product v w = (\<Sum> i \<in> UNIV. v $ i * w $ i)"
 
 
@@ -311,7 +311,7 @@
 
 definition%important "scaleR \<equiv> (\<lambda> r x. (\<chi> i. scaleR r (x$i)))"
 
-lemma vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)"
+lemma%important vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)"
   unfolding scaleR_vec_def by simp
 
 instance%unimportant
@@ -330,7 +330,7 @@
     (\<forall>x\<in>S. \<exists>A. (\<forall>i. open (A i) \<and> x$i \<in> A i) \<and>
       (\<forall>y. (\<forall>i. y$i \<in> A i) \<longrightarrow> y \<in> S))"
 
-instance proof
+instance proof%unimportant
   show "open (UNIV :: ('a ^ 'b) set)"
     unfolding open_vec_def by auto
 next
@@ -358,30 +358,30 @@
 
 end
 
-lemma open_vector_box: "\<forall>i. open (S i) \<Longrightarrow> open {x. \<forall>i. x $ i \<in> S i}"
+lemma%unimportant open_vector_box: "\<forall>i. open (S i) \<Longrightarrow> open {x. \<forall>i. x $ i \<in> S i}"
   unfolding open_vec_def by auto
 
-lemma open_vimage_vec_nth: "open S \<Longrightarrow> open ((\<lambda>x. x $ i) -` S)"
+lemma%unimportant open_vimage_vec_nth: "open S \<Longrightarrow> open ((\<lambda>x. x $ i) -` S)"
   unfolding open_vec_def
   apply clarify
   apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI, simp)
   done
 
-lemma closed_vimage_vec_nth: "closed S \<Longrightarrow> closed ((\<lambda>x. x $ i) -` S)"
+lemma%unimportant closed_vimage_vec_nth: "closed S \<Longrightarrow> closed ((\<lambda>x. x $ i) -` S)"
   unfolding closed_open vimage_Compl [symmetric]
   by (rule open_vimage_vec_nth)
 
-lemma closed_vector_box: "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}"
+lemma%unimportant closed_vector_box: "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}"
 proof -
   have "{x. \<forall>i. x $ i \<in> S i} = (\<Inter>i. (\<lambda>x. x $ i) -` S i)" by auto
   thus "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}"
     by (simp add: closed_INT closed_vimage_vec_nth)
 qed
 
-lemma tendsto_vec_nth [tendsto_intros]:
+lemma%important tendsto_vec_nth [tendsto_intros]:
   assumes "((\<lambda>x. f x) \<longlongrightarrow> a) net"
   shows "((\<lambda>x. f x $ i) \<longlongrightarrow> a $ i) net"
-proof (rule topological_tendstoI)
+proof%unimportant (rule topological_tendstoI)
   fix S assume "open S" "a $ i \<in> S"
   then have "open ((\<lambda>y. y $ i) -` S)" "a \<in> ((\<lambda>y. y $ i) -` S)"
     by (simp_all add: open_vimage_vec_nth)
@@ -391,13 +391,13 @@
     by simp
 qed
 
-lemma isCont_vec_nth [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x $ i) a"
+lemma%unimportant isCont_vec_nth [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x $ i) a"
   unfolding isCont_def by (rule tendsto_vec_nth)
 
-lemma vec_tendstoI:
+lemma%important vec_tendstoI:
   assumes "\<And>i. ((\<lambda>x. f x $ i) \<longlongrightarrow> a $ i) net"
   shows "((\<lambda>x. f x) \<longlongrightarrow> a) net"
-proof (rule topological_tendstoI)
+proof%unimportant (rule topological_tendstoI)
   fix S assume "open S" and "a \<in> S"
   then obtain A where A: "\<And>i. open (A i)" "\<And>i. a $ i \<in> A i"
     and S: "\<And>y. \<forall>i. y $ i \<in> A i \<Longrightarrow> y \<in> S"
@@ -410,13 +410,13 @@
     by (rule eventually_mono, simp add: S)
 qed
 
-lemma tendsto_vec_lambda [tendsto_intros]:
+lemma%unimportant tendsto_vec_lambda [tendsto_intros]:
   assumes "\<And>i. ((\<lambda>x. f x i) \<longlongrightarrow> a i) net"
   shows "((\<lambda>x. \<chi> i. f x i) \<longlongrightarrow> (\<chi> i. a i)) net"
   using assms by (simp add: vec_tendstoI)
 
-lemma open_image_vec_nth: assumes "open S" shows "open ((\<lambda>x. x $ i) ` S)"
-proof (rule openI)
+lemma%important open_image_vec_nth: assumes "open S" shows "open ((\<lambda>x. x $ i) ` S)"
+proof%unimportant (rule openI)
   fix a assume "a \<in> (\<lambda>x. x $ i) ` S"
   then obtain z where "a = z $ i" and "z \<in> S" ..
   then obtain A where A: "\<forall>i. open (A i) \<and> z $ i \<in> A i"
@@ -470,10 +470,10 @@
 instantiation%unimportant vec :: (metric_space, finite) metric_space
 begin
 
-lemma dist_vec_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
+lemma%important dist_vec_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
   unfolding dist_vec_def by (rule member_le_L2_set) simp_all
 
-instance proof
+instance proof%unimportant
   fix x y :: "'a ^ 'b"
   show "dist x y = 0 \<longleftrightarrow> x = y"
     unfolding dist_vec_def
@@ -532,15 +532,15 @@
 
 end
 
-lemma Cauchy_vec_nth:
+lemma%important Cauchy_vec_nth:
   "Cauchy (\<lambda>n. X n) \<Longrightarrow> Cauchy (\<lambda>n. X n $ i)"
   unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_vec_nth_le])
 
-lemma vec_CauchyI:
+lemma%important vec_CauchyI:
   fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n"
   assumes X: "\<And>i. Cauchy (\<lambda>n. X n $ i)"
   shows "Cauchy (\<lambda>n. X n)"
-proof (rule metric_CauchyI)
+proof%unimportant (rule metric_CauchyI)
   fix r :: real assume "0 < r"
   hence "0 < r / of_nat CARD('n)" (is "0 < ?s") by simp
   define N where "N i = (LEAST N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s)" for i
@@ -591,7 +591,7 @@
 
 definition%important "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
 
-instance proof
+instance proof%unimportant
   fix a :: real and x y :: "'a ^ 'b"
   show "norm x = 0 \<longleftrightarrow> x = 0"
     unfolding norm_vec_def
@@ -613,32 +613,32 @@
 
 end
 
-lemma norm_nth_le: "norm (x $ i) \<le> norm x"
+lemma%unimportant norm_nth_le: "norm (x $ i) \<le> norm x"
 unfolding norm_vec_def
 by (rule member_le_L2_set) simp_all
 
-lemma norm_le_componentwise_cart:
+lemma%important norm_le_componentwise_cart:
   fixes x :: "'a::real_normed_vector^'n"
   assumes "\<And>i. norm(x$i) \<le> norm(y$i)"
   shows "norm x \<le> norm y"
-  unfolding norm_vec_def
-  by (rule L2_set_mono) (auto simp: assms)
+  unfolding%unimportant norm_vec_def
+  by%unimportant (rule L2_set_mono) (auto simp: assms)
 
-lemma component_le_norm_cart: "\<bar>x$i\<bar> \<le> norm x"
+lemma%unimportant component_le_norm_cart: "\<bar>x$i\<bar> \<le> norm x"
   apply (simp add: norm_vec_def)
   apply (rule member_le_L2_set, simp_all)
   done
 
-lemma norm_bound_component_le_cart: "norm x \<le> e ==> \<bar>x$i\<bar> \<le> e"
+lemma%unimportant norm_bound_component_le_cart: "norm x \<le> e ==> \<bar>x$i\<bar> \<le> e"
   by (metis component_le_norm_cart order_trans)
 
-lemma norm_bound_component_lt_cart: "norm x < e ==> \<bar>x$i\<bar> < e"
+lemma%unimportant norm_bound_component_lt_cart: "norm x < e ==> \<bar>x$i\<bar> < e"
   by (metis component_le_norm_cart le_less_trans)
 
-lemma norm_le_l1_cart: "norm x \<le> sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
+lemma%unimportant norm_le_l1_cart: "norm x \<le> sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
   by (simp add: norm_vec_def L2_set_le_sum)
 
-lemma bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
+lemma%unimportant bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
 apply standard
 apply (rule vector_add_component)
 apply (rule vector_scaleR_component)
@@ -655,7 +655,7 @@
 
 definition%important "inner x y = sum (\<lambda>i. inner (x$i) (y$i)) UNIV"
 
-instance proof
+instance proof%unimportant
   fix r :: real and x y z :: "'a ^ 'b"
   show "inner x y = inner y x"
     unfolding inner_vec_def
@@ -686,13 +686,13 @@
 
 definition%important "axis k x = (\<chi> i. if i = k then x else 0)"
 
-lemma axis_nth [simp]: "axis i x $ i = x"
+lemma%unimportant axis_nth [simp]: "axis i x $ i = x"
   unfolding axis_def by simp
 
-lemma axis_eq_axis: "axis i x = axis j y \<longleftrightarrow> x = y \<and> i = j \<or> x = 0 \<and> y = 0"
+lemma%unimportant axis_eq_axis: "axis i x = axis j y \<longleftrightarrow> x = y \<and> i = j \<or> x = 0 \<and> y = 0"
   unfolding axis_def vec_eq_iff by auto
 
-lemma inner_axis_axis:
+lemma%unimportant inner_axis_axis:
   "inner (axis i x) (axis j y) = (if i = j then inner x y else 0)"
   unfolding inner_vec_def
   apply (cases "i = j")
@@ -702,10 +702,10 @@
   apply (rule sum.neutral, simp add: axis_def)
   done
 
-lemma inner_axis: "inner x (axis i y) = inner (x $ i) y"
+lemma%unimportant inner_axis: "inner x (axis i y) = inner (x $ i) y"
   by (simp add: inner_vec_def axis_def sum.remove [where x=i])
 
-lemma inner_axis': "inner(axis i y) x = inner y (x $ i)"
+lemma%unimportant inner_axis': "inner(axis i y) x = inner y (x $ i)"
   by (simp add: inner_axis inner_commute)
 
 instantiation%unimportant vec :: (euclidean_space, finite) euclidean_space
@@ -713,7 +713,7 @@
 
 definition%important "Basis = (\<Union>i. \<Union>u\<in>Basis. {axis i u})"
 
-instance proof
+instance proof%unimportant
   show "(Basis :: ('a ^ 'b) set) \<noteq> {}"
     unfolding Basis_vec_def by simp
 next
@@ -732,8 +732,8 @@
     by (simp add: inner_axis euclidean_all_zero_iff vec_eq_iff)
 qed
 
-proposition DIM_cart [simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
-proof -
+lemma%important DIM_cart [simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
+proof%unimportant -
   have "card (\<Union>i::'b. \<Union>u::'a\<in>Basis. {axis i u}) = (\<Sum>i::'b\<in>UNIV. card (\<Union>u::'a\<in>Basis. {axis i u}))"
     by (rule card_UN_disjoint) (auto simp: axis_eq_axis) 
   also have "... = CARD('b) * DIM('a)"
@@ -744,30 +744,30 @@
 
 end
 
-lemma norm_axis_1 [simp]: "norm (axis m (1::real)) = 1"
+lemma%unimportant norm_axis_1 [simp]: "norm (axis m (1::real)) = 1"
   by (simp add: inner_axis' norm_eq_1)
 
-lemma sum_norm_allsubsets_bound_cart:
+lemma%important sum_norm_allsubsets_bound_cart:
   fixes f:: "'a \<Rightarrow> real ^'n"
   assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (sum f Q) \<le> e"
   shows "sum (\<lambda>x. norm (f x)) P \<le> 2 * real CARD('n) *  e"
-  using sum_norm_allsubsets_bound[OF assms]
-  by simp
+  using%unimportant sum_norm_allsubsets_bound[OF assms]
+  by%unimportant simp
 
-lemma cart_eq_inner_axis: "a $ i = inner a (axis i 1)"
+lemma%unimportant cart_eq_inner_axis: "a $ i = inner a (axis i 1)"
   by (simp add: inner_axis)
 
-lemma axis_eq_0_iff [simp]:
+lemma%unimportant axis_eq_0_iff [simp]:
   shows "axis m x = 0 \<longleftrightarrow> x = 0"
   by (simp add: axis_def vec_eq_iff)
 
-lemma axis_in_Basis_iff [simp]: "axis i a \<in> Basis \<longleftrightarrow> a \<in> Basis"
+lemma%unimportant axis_in_Basis_iff [simp]: "axis i a \<in> Basis \<longleftrightarrow> a \<in> Basis"
   by (auto simp: Basis_vec_def axis_eq_axis)
 
 text\<open>Mapping each basis element to the corresponding finite index\<close>
 definition axis_index :: "('a::comm_ring_1)^'n \<Rightarrow> 'n" where "axis_index v \<equiv> SOME i. v = axis i 1"
 
-lemma axis_inverse:
+lemma%unimportant axis_inverse:
   fixes v :: "real^'n"
   assumes "v \<in> Basis"
   shows "\<exists>i. v = axis i 1"
@@ -778,20 +778,20 @@
     by (force simp add: vec_eq_iff)
 qed
 
-lemma axis_index:
+lemma%unimportant axis_index:
   fixes v :: "real^'n"
   assumes "v \<in> Basis"
   shows "v = axis (axis_index v) 1"
   by (metis (mono_tags) assms axis_inverse axis_index_def someI_ex)
 
-lemma axis_index_axis [simp]:
+lemma%unimportant axis_index_axis [simp]:
   fixes UU :: "real^'n"
   shows "(axis_index (axis u 1 :: real^'n)) = (u::'n)"
   by (simp add: axis_eq_axis axis_index_def)
 
 subsection%unimportant \<open>A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space\<close>
 
-lemma sum_cong_aux:
+lemma%unimportant sum_cong_aux:
   "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> sum f A = sum g A"
   by (auto intro: sum.cong)
 
@@ -823,22 +823,22 @@
 end
 \<close> "lift trivial vector statements to real arith statements"
 
-lemma vec_0[simp]: "vec 0 = 0" by vector
-lemma vec_1[simp]: "vec 1 = 1" by vector
+lemma%unimportant vec_0[simp]: "vec 0 = 0" by vector
+lemma%unimportant vec_1[simp]: "vec 1 = 1" by vector
 
-lemma vec_inj[simp]: "vec x = vec y \<longleftrightarrow> x = y" by vector
+lemma%unimportant vec_inj[simp]: "vec x = vec y \<longleftrightarrow> x = y" by vector
 
-lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
+lemma%unimportant vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
 
-lemma vec_add: "vec(x + y) = vec x + vec y"  by vector
-lemma vec_sub: "vec(x - y) = vec x - vec y" by vector
-lemma vec_cmul: "vec(c * x) = c *s vec x " by vector
-lemma vec_neg: "vec(- x) = - vec x " by vector
+lemma%unimportant vec_add: "vec(x + y) = vec x + vec y"  by vector
+lemma%unimportant vec_sub: "vec(x - y) = vec x - vec y" by vector
+lemma%unimportant vec_cmul: "vec(c * x) = c *s vec x " by vector
+lemma%unimportant vec_neg: "vec(- x) = - vec x " by vector
 
-lemma vec_scaleR: "vec(c * x) = c *\<^sub>R vec x"
+lemma%unimportant vec_scaleR: "vec(c * x) = c *\<^sub>R vec x"
   by vector
 
-lemma vec_sum:
+lemma%unimportant vec_sum:
   assumes "finite S"
   shows "vec(sum f S) = sum (vec \<circ> f) S"
   using assms
@@ -852,24 +852,24 @@
 
 text\<open>Obvious "component-pushing".\<close>
 
-lemma vec_component [simp]: "vec x $ i = x"
+lemma%unimportant vec_component [simp]: "vec x $ i = x"
   by vector
 
-lemma vector_mult_component [simp]: "(x * y)$i = x$i * y$i"
+lemma%unimportant vector_mult_component [simp]: "(x * y)$i = x$i * y$i"
   by vector
 
-lemma vector_smult_component [simp]: "(c *s y)$i = c * (y$i)"
+lemma%unimportant vector_smult_component [simp]: "(c *s y)$i = c * (y$i)"
   by vector
 
-lemma cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector
+lemma%unimportant cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector
 
-lemmas vector_component =
+lemmas%unimportant vector_component =
   vec_component vector_add_component vector_mult_component
   vector_smult_component vector_minus_component vector_uminus_component
   vector_scaleR_component cond_component
 
 
-subsection%important \<open>Some frequently useful arithmetic lemmas over vectors\<close>
+subsection%unimportant \<open>Some frequently useful arithmetic lemmas over vectors\<close>
 
 instance vec :: (semigroup_mult, finite) semigroup_mult
   by standard (vector mult.assoc)
@@ -1011,7 +1011,7 @@
 definition%important 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)"
+lemma%unimportant nth_map_matrix[simp]: "map_matrix f x $ i $ j = f (x $ i $ j)"
   by (simp add: map_matrix_def)
 
 definition%important matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m"
@@ -1034,17 +1034,17 @@
 definition%unimportant "rows(A::'a^'n^'m) = { row i A | i. i \<in> (UNIV :: 'm set)}"
 definition%unimportant "columns(A::'a^'n^'m) = { column i A | i. i \<in> (UNIV :: 'n set)}"
 
-lemma times0_left [simp]: "(0::'a::semiring_1^'n^'m) ** (A::'a ^'p^'n) = 0" 
+lemma%unimportant times0_left [simp]: "(0::'a::semiring_1^'n^'m) ** (A::'a ^'p^'n) = 0" 
   by (simp add: matrix_matrix_mult_def zero_vec_def)
 
-lemma times0_right [simp]: "(A::'a::semiring_1^'n^'m) ** (0::'a ^'p^'n) = 0" 
+lemma%unimportant times0_right [simp]: "(A::'a::semiring_1^'n^'m) ** (0::'a ^'p^'n) = 0" 
   by (simp add: matrix_matrix_mult_def zero_vec_def)
 
-lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def)
-lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)"
+lemma%unimportant mat_0[simp]: "mat 0 = 0" by (vector mat_def)
+lemma%unimportant matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)"
   by (vector matrix_matrix_mult_def sum.distrib[symmetric] field_simps)
 
-lemma matrix_mul_lid [simp]:
+lemma%unimportant matrix_mul_lid [simp]:
   fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
   shows "mat 1 ** A = A"
   apply (simp add: matrix_matrix_mult_def mat_def)
@@ -1053,7 +1053,7 @@
     mult_1_left mult_zero_left if_True UNIV_I)
   done
 
-lemma matrix_mul_rid [simp]:
+lemma%unimportant matrix_mul_rid [simp]:
   fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
   shows "A ** mat 1 = A"
   apply (simp add: matrix_matrix_mult_def mat_def)
@@ -1062,39 +1062,47 @@
     mult_1_right mult_zero_right if_True UNIV_I cong: if_cong)
   done
 
-proposition matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"
+lemma%unimportant matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"
   apply (vector matrix_matrix_mult_def sum_distrib_left sum_distrib_right mult.assoc)
   apply (subst sum.swap)
   apply simp
   done
 
-proposition matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
+lemma%unimportant matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
   apply (vector matrix_matrix_mult_def matrix_vector_mult_def
     sum_distrib_left sum_distrib_right mult.assoc)
   apply (subst sum.swap)
   apply simp
   done
 
-lemma scalar_matrix_assoc:
+lemma%unimportant scalar_matrix_assoc:
   fixes A :: "('a::real_algebra_1)^'m^'n"
   shows "k *\<^sub>R (A ** B) = (k *\<^sub>R A) ** B"
   by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff scaleR_sum_right)
 
-lemma matrix_scalar_ac:
+lemma%unimportant matrix_scalar_ac:
   fixes A :: "('a::real_algebra_1)^'m^'n"
   shows "A ** (k *\<^sub>R B) = k *\<^sub>R A ** B"
   by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff)
 
-lemma matrix_vector_mul_lid [simp]: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"
+lemma%unimportant matrix_vector_mul_lid [simp]: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"
   apply (vector matrix_vector_mult_def mat_def)
   apply (simp add: if_distrib if_distribR sum.delta' cong del: if_weak_cong)
   done
 
-lemma matrix_transpose_mul:
+lemma%unimportant matrix_transpose_mul:
     "transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)"
   by (simp add: matrix_matrix_mult_def transpose_def vec_eq_iff mult.commute)
 
-lemma matrix_eq:
+lemma%unimportant matrix_mult_transpose_dot_column:
+  shows "transpose A ** A = (\<chi> i j. inner (column i A) (column j A))"
+  by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def column_def inner_vec_def)
+
+lemma%unimportant matrix_mult_transpose_dot_row:
+  shows "A ** transpose A = (\<chi> i j. inner (row i A) (row j A))"
+  by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def)
+
+lemma%unimportant matrix_eq:
   fixes A B :: "'a::semiring_1 ^ 'n ^ 'm"
   shows "A = B \<longleftrightarrow>  (\<forall>x. A *v x = B *v x)" (is "?lhs \<longleftrightarrow> ?rhs")
   apply auto
@@ -1107,49 +1115,49 @@
     sum.delta[OF finite] cong del: if_weak_cong)
   done
 
-lemma matrix_vector_mul_component: "(A *v x)$k = inner (A$k) x"
+lemma%unimportant matrix_vector_mul_component: "(A *v x)$k = inner (A$k) x"
   by (simp add: matrix_vector_mult_def inner_vec_def)
 
-lemma dot_lmul_matrix: "inner ((x::real ^_) v* A) y = inner x (A *v y)"
+lemma%unimportant dot_lmul_matrix: "inner ((x::real ^_) v* A) y = inner x (A *v y)"
   apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def sum_distrib_right sum_distrib_left ac_simps)
   apply (subst sum.swap)
   apply simp
   done
 
-lemma transpose_mat [simp]: "transpose (mat n) = mat n"
+lemma%unimportant transpose_mat [simp]: "transpose (mat n) = mat n"
   by (vector transpose_def mat_def)
 
-lemma transpose_transpose [simp]: "transpose(transpose A) = A"
+lemma%unimportant transpose_transpose [simp]: "transpose(transpose A) = A"
   by (vector transpose_def)
 
-lemma row_transpose [simp]: "row i (transpose A) = column i A"
+lemma%unimportant row_transpose [simp]: "row i (transpose A) = column i A"
   by (simp add: row_def column_def transpose_def vec_eq_iff)
 
-lemma column_transpose [simp]: "column i (transpose A) = row i A"
+lemma%unimportant column_transpose [simp]: "column i (transpose A) = row i A"
   by (simp add: row_def column_def transpose_def vec_eq_iff)
 
-lemma rows_transpose [simp]: "rows(transpose A) = columns A"
+lemma%unimportant rows_transpose [simp]: "rows(transpose A) = columns A"
   by (auto simp add: rows_def columns_def intro: set_eqI)
 
-lemma columns_transpose [simp]: "columns(transpose A) = rows A"
+lemma%unimportant columns_transpose [simp]: "columns(transpose A) = rows A"
   by (metis transpose_transpose rows_transpose)
 
-lemma transpose_scalar: "transpose (k *\<^sub>R A) = k *\<^sub>R transpose A"
+lemma%unimportant transpose_scalar: "transpose (k *\<^sub>R A) = k *\<^sub>R transpose A"
   unfolding transpose_def
   by (simp add: vec_eq_iff)
 
-lemma transpose_iff [iff]: "transpose A = transpose B \<longleftrightarrow> A = B"
+lemma%unimportant transpose_iff [iff]: "transpose A = transpose B \<longleftrightarrow> A = B"
   by (metis transpose_transpose)
 
-lemma matrix_mult_sum:
+lemma%unimportant matrix_mult_sum:
   "(A::'a::comm_semiring_1^'n^'m) *v x = sum (\<lambda>i. (x$i) *s column i A) (UNIV:: 'n set)"
   by (simp add: matrix_vector_mult_def vec_eq_iff column_def mult.commute)
 
-lemma vector_componentwise:
+lemma%unimportant vector_componentwise:
   "(x::'a::ring_1^'n) = (\<chi> j. \<Sum>i\<in>UNIV. (x$i) * (axis i 1 :: 'a^'n) $ j)"
   by (simp add: axis_def if_distrib sum.If_cases vec_eq_iff)
 
-lemma basis_expansion: "sum (\<lambda>i. (x$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)"
+lemma%unimportant basis_expansion: "sum (\<lambda>i. (x$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)"
   by (auto simp add: axis_def vec_eq_iff if_distrib sum.If_cases cong del: if_weak_cong)
 
 
@@ -1158,51 +1166,51 @@
 definition%important matrix :: "('a::{plus,times, one, zero}^'m \<Rightarrow> 'a ^ 'n) \<Rightarrow> 'a^'m^'n"
   where "matrix f = (\<chi> i j. (f(axis j 1))$i)"
 
-lemma matrix_id_mat_1: "matrix id = mat 1"
+lemma%unimportant matrix_id_mat_1: "matrix id = mat 1"
   by (simp add: mat_def matrix_def axis_def)
 
-lemma matrix_scaleR: "(matrix ((*\<^sub>R) r)) = mat r"
+lemma%unimportant matrix_scaleR: "(matrix ((*\<^sub>R) r)) = mat r"
   by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong)
 
-lemma matrix_vector_mul_linear[intro, simp]: "linear (\<lambda>x. A *v (x::'a::real_algebra_1 ^ _))"
+lemma%unimportant matrix_vector_mul_linear[intro, simp]: "linear (\<lambda>x. A *v (x::'a::real_algebra_1 ^ _))"
   by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff field_simps sum_distrib_left
       sum.distrib scaleR_right.sum)
 
-lemma vector_matrix_left_distrib [algebra_simps]:
+lemma%unimportant vector_matrix_left_distrib [algebra_simps]:
   shows "(x + y) v* A = x v* A + y v* A"
   unfolding vector_matrix_mult_def
   by (simp add: algebra_simps sum.distrib vec_eq_iff)
 
-lemma matrix_vector_right_distrib [algebra_simps]:
+lemma%unimportant matrix_vector_right_distrib [algebra_simps]:
   "A *v (x + y) = A *v x + A *v y"
   by (vector matrix_vector_mult_def sum.distrib distrib_left)
 
-lemma matrix_vector_mult_diff_distrib [algebra_simps]:
+lemma%unimportant matrix_vector_mult_diff_distrib [algebra_simps]:
   fixes A :: "'a::ring_1^'n^'m"
   shows "A *v (x - y) = A *v x - A *v y"
   by (vector matrix_vector_mult_def sum_subtractf right_diff_distrib)
 
-lemma matrix_vector_mult_scaleR[algebra_simps]:
+lemma%unimportant matrix_vector_mult_scaleR[algebra_simps]:
   fixes A :: "real^'n^'m"
   shows "A *v (c *\<^sub>R x) = c *\<^sub>R (A *v x)"
   using linear_iff matrix_vector_mul_linear by blast
 
-lemma matrix_vector_mult_0_right [simp]: "A *v 0 = 0"
+lemma%unimportant matrix_vector_mult_0_right [simp]: "A *v 0 = 0"
   by (simp add: matrix_vector_mult_def vec_eq_iff)
 
-lemma matrix_vector_mult_0 [simp]: "0 *v w = 0"
+lemma%unimportant matrix_vector_mult_0 [simp]: "0 *v w = 0"
   by (simp add: matrix_vector_mult_def vec_eq_iff)
 
-lemma matrix_vector_mult_add_rdistrib [algebra_simps]:
+lemma%unimportant matrix_vector_mult_add_rdistrib [algebra_simps]:
   "(A + B) *v x = (A *v x) + (B *v x)"
   by (vector matrix_vector_mult_def sum.distrib distrib_right)
 
-lemma matrix_vector_mult_diff_rdistrib [algebra_simps]:
+lemma%unimportant matrix_vector_mult_diff_rdistrib [algebra_simps]:
   fixes A :: "'a :: ring_1^'n^'m"
   shows "(A - B) *v x = (A *v x) - (B *v x)"
   by (vector matrix_vector_mult_def sum_subtractf left_diff_distrib)
 
-lemma matrix_vector_column:
+lemma%unimportant matrix_vector_column:
   "(A::'a::comm_semiring_1^'n^_) *v x = sum (\<lambda>i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)"
   by (simp add: matrix_vector_mult_def transpose_def vec_eq_iff mult.commute)
 
@@ -1215,17 +1223,17 @@
   "matrix_inv(A:: 'a::semiring_1^'n^'m) =
     (SOME A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
 
-lemma inj_matrix_vector_mult:
+lemma%unimportant inj_matrix_vector_mult:
   fixes A::"'a::field^'n^'m"
   assumes "invertible A"
   shows "inj ((*v) A)"
   by (metis assms inj_on_inverseI invertible_def matrix_vector_mul_assoc matrix_vector_mul_lid)
 
-lemma scalar_invertible:
+lemma%important scalar_invertible:
   fixes A :: "('a::real_algebra_1)^'m^'n"
   assumes "k \<noteq> 0" and "invertible A"
   shows "invertible (k *\<^sub>R A)"
-proof -
+proof%unimportant -
   obtain A' where "A ** A' = mat 1" and "A' ** A = mat 1"
     using assms unfolding invertible_def by auto
   with \<open>k \<noteq> 0\<close>
@@ -1235,50 +1243,50 @@
     unfolding invertible_def by auto
 qed
 
-lemma scalar_invertible_iff:
+lemma%unimportant scalar_invertible_iff:
   fixes A :: "('a::real_algebra_1)^'m^'n"
   assumes "k \<noteq> 0" and "invertible A"
   shows "invertible (k *\<^sub>R A) \<longleftrightarrow> k \<noteq> 0 \<and> invertible A"
   by (simp add: assms scalar_invertible)
 
-lemma vector_transpose_matrix [simp]: "x v* transpose A = A *v x"
+lemma%unimportant vector_transpose_matrix [simp]: "x v* transpose A = A *v x"
   unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
   by simp
 
-lemma transpose_matrix_vector [simp]: "transpose A *v x = x v* A"
+lemma%unimportant transpose_matrix_vector [simp]: "transpose A *v x = x v* A"
   unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
   by simp
 
-lemma vector_scalar_commute:
+lemma%unimportant vector_scalar_commute:
   fixes A :: "'a::{field}^'m^'n"
   shows "A *v (c *s x) = c *s (A *v x)"
   by (simp add: vector_scalar_mult_def matrix_vector_mult_def mult_ac sum_distrib_left)
 
-lemma scalar_vector_matrix_assoc:
+lemma%unimportant scalar_vector_matrix_assoc:
   fixes k :: "'a::{field}" and x :: "'a::{field}^'n" and A :: "'a^'m^'n"
   shows "(k *s x) v* A = k *s (x v* A)"
   by (metis transpose_matrix_vector vector_scalar_commute)
  
-lemma vector_matrix_mult_0 [simp]: "0 v* A = 0"
+lemma%unimportant vector_matrix_mult_0 [simp]: "0 v* A = 0"
   unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
 
-lemma vector_matrix_mult_0_right [simp]: "x v* 0 = 0"
+lemma%unimportant vector_matrix_mult_0_right [simp]: "x v* 0 = 0"
   unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
 
-lemma vector_matrix_mul_rid [simp]:
+lemma%unimportant vector_matrix_mul_rid [simp]:
   fixes v :: "('a::semiring_1)^'n"
   shows "v v* mat 1 = v"
   by (metis matrix_vector_mul_lid transpose_mat vector_transpose_matrix)
 
-lemma scaleR_vector_matrix_assoc:
+lemma%unimportant scaleR_vector_matrix_assoc:
   fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
   shows "(k *\<^sub>R x) v* A = k *\<^sub>R (x v* A)"
   by (metis matrix_vector_mult_scaleR transpose_matrix_vector)
 
-lemma vector_scaleR_matrix_ac:
+lemma%important vector_scaleR_matrix_ac:
   fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
   shows "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
-proof -
+proof%unimportant -
   have "x v* (k *\<^sub>R A) = (k *\<^sub>R x) v* A"
     unfolding vector_matrix_mult_def
     by (simp add: algebra_simps)
--- a/src/HOL/Analysis/Further_Topology.thy	Wed Jan 16 21:27:33 2019 +0000
+++ b/src/HOL/Analysis/Further_Topology.thy	Thu Jan 17 15:50:28 2019 +0000
@@ -1,4 +1,4 @@
-section%important \<open>Extending Continous Maps, Invariance of Domain, etc\<close>
+section%important \<open>Extending Continous Maps, Invariance of Domain, etc\<close> (*FIX rename? *)
 
 text\<open>Ported from HOL Light (moretop.ml) by L C Paulson\<close>
 
@@ -8,13 +8,13 @@
 
 subsection%important\<open>A map from a sphere to a higher dimensional sphere is nullhomotopic\<close>
 
-lemma%important spheremap_lemma1:
+lemma spheremap_lemma1:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   assumes "subspace S" "subspace T" and dimST: "dim S < dim T"
       and "S \<subseteq> T"
       and diff_f: "f differentiable_on sphere 0 1 \<inter> S"
     shows "f ` (sphere 0 1 \<inter> S) \<noteq> sphere 0 1 \<inter> T"
-proof%unimportant
+proof
   assume fim: "f ` (sphere 0 1 \<inter> S) = sphere 0 1 \<inter> T"
   have inS: "\<And>x. \<lbrakk>x \<in> S; x \<noteq> 0\<rbrakk> \<Longrightarrow> (x /\<^sub>R norm x) \<in> S"
     using subspace_mul \<open>subspace S\<close> by blast
@@ -158,14 +158,14 @@
 qed
 
 
-lemma%important spheremap_lemma2:
+lemma spheremap_lemma2:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   assumes ST: "subspace S" "subspace T" "dim S < dim T"
       and "S \<subseteq> T"
       and contf: "continuous_on (sphere 0 1 \<inter> S) f"
       and fim: "f ` (sphere 0 1 \<inter> S) \<subseteq> sphere 0 1 \<inter> T"
     shows "\<exists>c. homotopic_with (\<lambda>x. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) f (\<lambda>x. c)"
-proof%unimportant -
+proof -
   have [simp]: "\<And>x. \<lbrakk>norm x = 1; x \<in> S\<rbrakk> \<Longrightarrow> norm (f x) = 1"
     using fim by (simp add: image_subset_iff)
   have "compact (sphere 0 1 \<inter> S)"
@@ -252,11 +252,11 @@
 qed
 
 
-lemma%important spheremap_lemma3:
+lemma spheremap_lemma3:
   assumes "bounded S" "convex S" "subspace U" and affSU: "aff_dim S \<le> dim U"
   obtains T where "subspace T" "T \<subseteq> U" "S \<noteq> {} \<Longrightarrow> aff_dim T = aff_dim S"
                   "(rel_frontier S) homeomorphic (sphere 0 1 \<inter> T)"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
   case True
   with \<open>subspace U\<close> subspace_0 show ?thesis
     by (rule_tac T = "{0}" in that) auto
@@ -300,14 +300,14 @@
 qed
 
 
-proposition%important inessential_spheremap_lowdim_gen:
+proposition inessential_spheremap_lowdim_gen:
   fixes f :: "'M::euclidean_space \<Rightarrow> 'a::euclidean_space"
   assumes "convex S" "bounded S" "convex T" "bounded T"
       and affST: "aff_dim S < aff_dim T"
       and contf: "continuous_on (rel_frontier S) f"
       and fim: "f ` (rel_frontier S) \<subseteq> rel_frontier T"
   obtains c where "homotopic_with (\<lambda>z. True) (rel_frontier S) (rel_frontier T) f (\<lambda>x. c)"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
   case True
   then show ?thesis
     by (simp add: that)
@@ -350,7 +350,7 @@
   qed
 qed
 
-lemma%unimportant inessential_spheremap_lowdim:
+lemma inessential_spheremap_lowdim:
   fixes f :: "'M::euclidean_space \<Rightarrow> 'a::euclidean_space"
   assumes
    "DIM('M) < DIM('a)" and f: "continuous_on (sphere a r) f" "f ` (sphere a r) \<subseteq> (sphere b s)"
@@ -379,7 +379,7 @@
 
 subsection%important\<open> Some technical lemmas about extending maps from cell complexes\<close>
 
-lemma%unimportant extending_maps_Union_aux:
+lemma extending_maps_Union_aux:
   assumes fin: "finite \<F>"
       and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S"
       and "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>; S \<noteq> T\<rbrakk> \<Longrightarrow> S \<inter> T \<subseteq> K"
@@ -410,7 +410,7 @@
     done
 qed
 
-lemma%unimportant extending_maps_Union:
+lemma extending_maps_Union:
   assumes fin: "finite \<F>"
       and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>g. continuous_on S g \<and> g ` S \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
       and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S"
@@ -422,14 +422,14 @@
 by (metis K psubsetI)
 
 
-lemma%important extend_map_lemma:
+lemma extend_map_lemma:
   assumes "finite \<F>" "\<G> \<subseteq> \<F>" "convex T" "bounded T"
       and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
       and aff: "\<And>X. X \<in> \<F> - \<G> \<Longrightarrow> aff_dim X < aff_dim T"
       and face: "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>\<rbrakk> \<Longrightarrow> (S \<inter> T) face_of S \<and> (S \<inter> T) face_of T"
       and contf: "continuous_on (\<Union>\<G>) f" and fim: "f ` (\<Union>\<G>) \<subseteq> rel_frontier T"
   obtains g where "continuous_on (\<Union>\<F>) g" "g ` (\<Union>\<F>) \<subseteq> rel_frontier T" "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> g x = f x"
-proof%unimportant (cases "\<F> - \<G> = {}")
+proof (cases "\<F> - \<G> = {}")
   case True
   then have "\<Union>\<F> \<subseteq> \<Union>\<G>"
     by (simp add: Union_mono)
@@ -608,7 +608,7 @@
     using extendf [of i] unfolding eq by (metis that)
 qed
 
-lemma%unimportant extend_map_lemma_cofinite0:
+lemma extend_map_lemma_cofinite0:
   assumes "finite \<F>"
       and "pairwise (\<lambda>S T. S \<inter> T \<subseteq> K) \<F>"
       and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (S - {a}) g \<and> g ` (S - {a}) \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
@@ -665,7 +665,7 @@
 qed
 
 
-lemma%unimportant extend_map_lemma_cofinite1:
+lemma extend_map_lemma_cofinite1:
 assumes "finite \<F>"
     and \<F>: "\<And>X. X \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (X - {a}) g \<and> g ` (X - {a}) \<subseteq> T \<and> (\<forall>x \<in> X \<inter> K. g x = h x)"
     and clo: "\<And>X. X \<in> \<F> \<Longrightarrow> closed X"
@@ -695,7 +695,7 @@
 qed
 
 
-lemma%important extend_map_lemma_cofinite:
+lemma extend_map_lemma_cofinite:
   assumes "finite \<F>" "\<G> \<subseteq> \<F>" and T: "convex T" "bounded T"
       and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
       and contf: "continuous_on (\<Union>\<G>) f" and fim: "f ` (\<Union>\<G>) \<subseteq> rel_frontier T"
@@ -704,7 +704,7 @@
   obtains C g where
      "finite C" "disjnt C (\<Union>\<G>)" "card C \<le> card \<F>" "continuous_on (\<Union>\<F> - C) g"
      "g ` (\<Union> \<F> - C) \<subseteq> rel_frontier T" "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> g x = f x"
-proof%unimportant -
+proof -
   define \<H> where "\<H> \<equiv> \<G> \<union> {D. \<exists>C \<in> \<F> - \<G>. D face_of C \<and> aff_dim D < aff_dim T}"
   have "finite \<G>"
     using assms finite_subset by blast
@@ -869,7 +869,7 @@
 qed
 
 text\<open>The next two proofs are similar\<close>
-theorem%important extend_map_cell_complex_to_sphere:
+theorem extend_map_cell_complex_to_sphere:
   assumes "finite \<F>" and S: "S \<subseteq> \<Union>\<F>" "closed S" and T: "convex T" "bounded T"
       and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
       and aff: "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X < aff_dim T"
@@ -877,7 +877,7 @@
       and contf: "continuous_on S f" and fim: "f ` S \<subseteq> rel_frontier T"
   obtains g where "continuous_on (\<Union>\<F>) g"
      "g ` (\<Union>\<F>) \<subseteq> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-proof%unimportant -
+proof -
   obtain V g where "S \<subseteq> V" "open V" "continuous_on V g" and gim: "g ` V \<subseteq> rel_frontier T" and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     using neighbourhood_extension_into_ANR [OF contf fim _ \<open>closed S\<close>] ANR_rel_frontier_convex T by blast
   have "compact S"
@@ -924,7 +924,7 @@
 qed
 
 
-theorem%important extend_map_cell_complex_to_sphere_cofinite:
+theorem extend_map_cell_complex_to_sphere_cofinite:
   assumes "finite \<F>" and S: "S \<subseteq> \<Union>\<F>" "closed S" and T: "convex T" "bounded T"
       and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
       and aff: "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> aff_dim T"
@@ -932,7 +932,7 @@
       and contf: "continuous_on S f" and fim: "f ` S \<subseteq> rel_frontier T"
   obtains C g where "finite C" "disjnt C S" "continuous_on (\<Union>\<F> - C) g"
      "g ` (\<Union>\<F> - C) \<subseteq> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-proof%unimportant -
+proof -
   obtain V g where "S \<subseteq> V" "open V" "continuous_on V g" and gim: "g ` V \<subseteq> rel_frontier T" and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     using neighbourhood_extension_into_ANR [OF contf fim _ \<open>closed S\<close>] ANR_rel_frontier_convex T by blast
   have "compact S"
@@ -993,10 +993,10 @@
 
 subsection%important\<open> Special cases and corollaries involving spheres\<close>
 
-lemma%unimportant disjnt_Diff1: "X \<subseteq> Y' \<Longrightarrow> disjnt (X - Y) (X' - Y')"
+lemma disjnt_Diff1: "X \<subseteq> Y' \<Longrightarrow> disjnt (X - Y) (X' - Y')"
   by (auto simp: disjnt_def)
 
-proposition%important extend_map_affine_to_sphere_cofinite_simple:
+proposition extend_map_affine_to_sphere_cofinite_simple:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "compact S" "convex U" "bounded U"
       and aff: "aff_dim T \<le> aff_dim U"
@@ -1005,7 +1005,7 @@
  obtains K g where "finite K" "K \<subseteq> T" "disjnt K S" "continuous_on (T - K) g"
                    "g ` (T - K) \<subseteq> rel_frontier U"
                    "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-proof%unimportant -
+proof -
   have "\<exists>K g. finite K \<and> disjnt K S \<and> continuous_on (T - K) g \<and>
               g ` (T - K) \<subseteq> rel_frontier U \<and> (\<forall>x \<in> S. g x = f x)"
        if "affine T" "S \<subseteq> T" and aff: "aff_dim T \<le> aff_dim U"  for T
@@ -1144,14 +1144,14 @@
 
 (*Up to extend_map_affine_to_sphere_cofinite_gen*)
 
-lemma%important extend_map_affine_to_sphere1:
+lemma extend_map_affine_to_sphere1:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::topological_space"
   assumes "finite K" "affine U" and contf: "continuous_on (U - K) f"
       and fim: "f ` (U - K) \<subseteq> T"
       and comps: "\<And>C. \<lbrakk>C \<in> components(U - S); C \<inter> K \<noteq> {}\<rbrakk> \<Longrightarrow> C \<inter> L \<noteq> {}"
       and clo: "closedin (subtopology euclidean U) S" and K: "disjnt K S" "K \<subseteq> U"
   obtains g where "continuous_on (U - L) g" "g ` (U - L) \<subseteq> T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-proof%unimportant (cases "K = {}")
+proof (cases "K = {}")
   case True
   then show ?thesis
     by (metis Diff_empty Diff_subset contf fim continuous_on_subset image_subsetI rev_image_eqI subset_iff that)
@@ -1436,7 +1436,7 @@
 qed
 
 
-lemma%important extend_map_affine_to_sphere2:
+lemma extend_map_affine_to_sphere2:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "compact S" "convex U" "bounded U" "affine T" "S \<subseteq> T"
       and affTU: "aff_dim T \<le> aff_dim U"
@@ -1446,7 +1446,7 @@
     obtains K g where "finite K" "K \<subseteq> L" "K \<subseteq> T" "disjnt K S"
                       "continuous_on (T - K) g" "g ` (T - K) \<subseteq> rel_frontier U"
                       "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-proof%unimportant -
+proof -
   obtain K g where K: "finite K" "K \<subseteq> T" "disjnt K S"
                and contg: "continuous_on (T - K) g"
                and gim: "g ` (T - K) \<subseteq> rel_frontier U"
@@ -1490,7 +1490,7 @@
 qed
 
 
-proposition%important extend_map_affine_to_sphere_cofinite_gen:
+proposition extend_map_affine_to_sphere_cofinite_gen:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes SUT: "compact S" "convex U" "bounded U" "affine T" "S \<subseteq> T"
       and aff: "aff_dim T \<le> aff_dim U"
@@ -1500,7 +1500,7 @@
  obtains K g where "finite K" "K \<subseteq> L" "K \<subseteq> T" "disjnt K S" "continuous_on (T - K) g"
                    "g ` (T - K) \<subseteq> rel_frontier U"
                    "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
   case True
   show ?thesis
   proof (cases "rel_frontier U = {}")
@@ -1645,7 +1645,7 @@
 qed
 
 
-corollary%important extend_map_affine_to_sphere_cofinite:
+corollary extend_map_affine_to_sphere_cofinite:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes SUT: "compact S" "affine T" "S \<subseteq> T"
       and aff: "aff_dim T \<le> DIM('b)" and "0 \<le> r"
@@ -1654,7 +1654,7 @@
       and dis: "\<And>C. \<lbrakk>C \<in> components(T - S); bounded C\<rbrakk> \<Longrightarrow> C \<inter> L \<noteq> {}"
   obtains K g where "finite K" "K \<subseteq> L" "K \<subseteq> T" "disjnt K S" "continuous_on (T - K) g"
                     "g ` (T - K) \<subseteq> sphere a r" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-proof%unimportant (cases "r = 0")
+proof (cases "r = 0")
   case True
   with fim show ?thesis
     by (rule_tac K="{}" and g = "\<lambda>x. a" in that) (auto simp: continuous_on_const)
@@ -1670,7 +1670,7 @@
     done
 qed
 
-corollary%important extend_map_UNIV_to_sphere_cofinite:
+corollary extend_map_UNIV_to_sphere_cofinite:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes aff: "DIM('a) \<le> DIM('b)" and "0 \<le> r"
       and SUT: "compact S"
@@ -1684,7 +1684,7 @@
  apply (auto simp: assms that Compl_eq_Diff_UNIV [symmetric])
 done
 
-corollary%important extend_map_UNIV_to_sphere_no_bounded_component:
+corollary extend_map_UNIV_to_sphere_no_bounded_component:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes aff: "DIM('a) \<le> DIM('b)" and "0 \<le> r"
       and SUT: "compact S"
@@ -1696,14 +1696,14 @@
    apply (auto simp: that dest: dis)
 done
 
-theorem%important Borsuk_separation_theorem_gen:
+theorem Borsuk_separation_theorem_gen:
   fixes S :: "'a::euclidean_space set"
   assumes "compact S"
     shows "(\<forall>c \<in> components(- S). \<not>bounded c) \<longleftrightarrow>
            (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::'a) 1
                 \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)))"
        (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume L [rule_format]: ?lhs
   show ?rhs
   proof clarify
@@ -1734,14 +1734,14 @@
 qed
 
 
-corollary%important Borsuk_separation_theorem:
+corollary Borsuk_separation_theorem:
   fixes S :: "'a::euclidean_space set"
   assumes "compact S" and 2: "2 \<le> DIM('a)"
     shows "connected(- S) \<longleftrightarrow>
            (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::'a) 1
                 \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)))"
        (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume L: ?lhs
   show ?rhs
   proof (cases "S = {}")
@@ -1764,7 +1764,7 @@
 qed
 
 
-lemma%unimportant homotopy_eqv_separation:
+lemma homotopy_eqv_separation:
   fixes S :: "'a::euclidean_space set" and T :: "'a set"
   assumes "S homotopy_eqv T" and "compact S" and "compact T"
   shows "connected(- S) \<longleftrightarrow> connected(- T)"
@@ -1783,11 +1783,11 @@
   qed
 qed
 
-lemma%important Jordan_Brouwer_separation:
+proposition Jordan_Brouwer_separation:
   fixes S :: "'a::euclidean_space set" and a::'a
   assumes hom: "S homeomorphic sphere a r" and "0 < r"
     shows "\<not> connected(- S)"
-proof%unimportant -
+proof -
   have "- sphere a r \<inter> ball a r \<noteq> {}"
     using \<open>0 < r\<close> by (simp add: Int_absorb1 subset_eq)
   moreover
@@ -1817,11 +1817,11 @@
 qed
 
 
-lemma%important Jordan_Brouwer_frontier:
+proposition Jordan_Brouwer_frontier:
   fixes S :: "'a::euclidean_space set" and a::'a
   assumes S: "S homeomorphic sphere a r" and T: "T \<in> components(- S)" and 2: "2 \<le> DIM('a)"
     shows "frontier T = S"
-proof%unimportant (cases r rule: linorder_cases)
+proof (cases r rule: linorder_cases)
   assume "r < 0"
   with S T show ?thesis by auto
 next
@@ -1866,11 +1866,11 @@
   qed (rule T)
 qed
 
-lemma%important Jordan_Brouwer_nonseparation:
+proposition Jordan_Brouwer_nonseparation:
   fixes S :: "'a::euclidean_space set" and a::'a
   assumes S: "S homeomorphic sphere a r" and "T \<subset> S" and 2: "2 \<le> DIM('a)"
     shows "connected(- T)"
-proof%unimportant -
+proof -
   have *: "connected(C \<union> (S - T))" if "C \<in> components(- S)" for C
   proof (rule connected_intermediate_closure)
     show "connected C"
@@ -1894,7 +1894,7 @@
 
 subsection%important\<open> Invariance of domain and corollaries\<close>
 
-lemma%unimportant invariance_of_domain_ball:
+lemma invariance_of_domain_ball:
   fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
   assumes contf: "continuous_on (cball a r) f" and "0 < r"
      and inj: "inj_on f (cball a r)"
@@ -1983,12 +1983,12 @@
 
 
 text\<open>Proved by L. E. J. Brouwer (1912)\<close>
-theorem%important invariance_of_domain:
+theorem invariance_of_domain:
   fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
   assumes "continuous_on S f" "open S" "inj_on f S"
     shows "open(f ` S)"
   unfolding open_subopen [of "f`S"]
-proof%unimportant clarify
+proof clarify
   fix a
   assume "a \<in> S"
   obtain \<delta> where "\<delta> > 0" and \<delta>: "cball a \<delta> \<subseteq> S"
@@ -2004,7 +2004,7 @@
   qed
 qed
 
-lemma%unimportant inv_of_domain_ss0:
+lemma inv_of_domain_ss0:
   fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
   assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \<subseteq> S"
       and "subspace S" and dimS: "dim S = DIM('b::euclidean_space)"
@@ -2049,7 +2049,7 @@
     by (metis (no_types, hide_lams) homeomorphism_imp_open_map homhk image_comp open_openin subtopology_UNIV)
 qed
 
-lemma%unimportant inv_of_domain_ss1:
+lemma inv_of_domain_ss1:
   fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
   assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \<subseteq> S"
       and "subspace S"
@@ -2090,14 +2090,14 @@
 qed
 
 
-corollary%important invariance_of_domain_subspaces:
+corollary invariance_of_domain_subspaces:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes ope: "openin (subtopology euclidean U) S"
       and "subspace U" "subspace V" and VU: "dim V \<le> dim U"
       and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
       and injf: "inj_on f S"
     shows "openin (subtopology euclidean V) (f ` S)"
-proof%unimportant -
+proof -
   obtain V' where "subspace V'" "V' \<subseteq> U" "dim V' = dim V"
     using choose_subspace_of_subspace [OF VU]
     by (metis span_eq_iff \<open>subspace U\<close>)
@@ -2134,14 +2134,14 @@
   qed
 qed
 
-corollary%important invariance_of_dimension_subspaces:
+corollary invariance_of_dimension_subspaces:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes ope: "openin (subtopology euclidean U) S"
       and "subspace U" "subspace V"
       and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
       and injf: "inj_on f S" and "S \<noteq> {}"
     shows "dim U \<le> dim V"
-proof%unimportant -
+proof -
   have "False" if "dim V < dim U"
   proof -
     obtain T where "subspace T" "T \<subseteq> U" "dim T = dim V"
@@ -2174,14 +2174,14 @@
     using not_less by blast
 qed
 
-corollary%important invariance_of_domain_affine_sets:
+corollary invariance_of_domain_affine_sets:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes ope: "openin (subtopology euclidean U) S"
       and aff: "affine U" "affine V" "aff_dim V \<le> aff_dim U"
       and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
       and injf: "inj_on f S"
     shows "openin (subtopology euclidean V) (f ` S)"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
   case True
   then show ?thesis by auto
 next
@@ -2209,14 +2209,14 @@
     by (metis (no_types, lifting) homeomorphism_imp_open_map homeomorphism_translation image_comp translation_galois)
 qed
 
-corollary%important invariance_of_dimension_affine_sets:
+corollary invariance_of_dimension_affine_sets:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes ope: "openin (subtopology euclidean U) S"
       and aff: "affine U" "affine V"
       and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
       and injf: "inj_on f S" and "S \<noteq> {}"
     shows "aff_dim U \<le> aff_dim V"
-proof%unimportant -
+proof -
   obtain a b where "a \<in> S" "a \<in> U" "b \<in> V"
     using \<open>S \<noteq> {}\<close> fim ope openin_contains_cball by fastforce
   have "dim ((+) (- a) ` U) \<le> dim ((+) (- b) ` V)"
@@ -2238,7 +2238,7 @@
     by (metis \<open>a \<in> U\<close> \<open>b \<in> V\<close> aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
 qed
 
-corollary%important invariance_of_dimension:
+corollary invariance_of_dimension:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes contf: "continuous_on S f" and "open S"
       and injf: "inj_on f S" and "S \<noteq> {}"
@@ -2247,7 +2247,7 @@
   by auto
 
 
-corollary%important continuous_injective_image_subspace_dim_le:
+corollary continuous_injective_image_subspace_dim_le:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "subspace S" "subspace T"
       and contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
@@ -2256,7 +2256,7 @@
   apply (rule invariance_of_dimension_subspaces [of S S _ f])
   using%unimportant assms by (auto simp: subspace_affine)
 
-lemma%unimportant invariance_of_dimension_convex_domain:
+lemma invariance_of_dimension_convex_domain:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "convex S"
       and contf: "continuous_on S f" and fim: "f ` S \<subseteq> affine hull T"
@@ -2285,7 +2285,7 @@
 qed
 
 
-lemma%unimportant homeomorphic_convex_sets_le:
+lemma homeomorphic_convex_sets_le:
   assumes "convex S" "S homeomorphic T"
   shows "aff_dim S \<le> aff_dim T"
 proof -
@@ -2302,23 +2302,23 @@
   qed
 qed
 
-lemma%unimportant homeomorphic_convex_sets:
+lemma homeomorphic_convex_sets:
   assumes "convex S" "convex T" "S homeomorphic T"
   shows "aff_dim S = aff_dim T"
   by (meson assms dual_order.antisym homeomorphic_convex_sets_le homeomorphic_sym)
 
-lemma%unimportant homeomorphic_convex_compact_sets_eq:
+lemma homeomorphic_convex_compact_sets_eq:
   assumes "convex S" "compact S" "convex T" "compact T"
   shows "S homeomorphic T \<longleftrightarrow> aff_dim S = aff_dim T"
   by (meson assms homeomorphic_convex_compact_sets homeomorphic_convex_sets)
 
-lemma%unimportant invariance_of_domain_gen:
+lemma invariance_of_domain_gen:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "open S" "continuous_on S f" "inj_on f S" "DIM('b) \<le> DIM('a)"
     shows "open(f ` S)"
   using invariance_of_domain_subspaces [of UNIV S UNIV f] assms by auto
 
-lemma%unimportant injective_into_1d_imp_open_map_UNIV:
+lemma injective_into_1d_imp_open_map_UNIV:
   fixes f :: "'a::euclidean_space \<Rightarrow> real"
   assumes "open T" "continuous_on S f" "inj_on f S" "T \<subseteq> S"
     shows "open (f ` T)"
@@ -2326,7 +2326,7 @@
   using assms apply (auto simp: elim: continuous_on_subset subset_inj_on)
   done
 
-lemma%unimportant continuous_on_inverse_open:
+lemma continuous_on_inverse_open:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" and gf: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
     shows "continuous_on (f ` S) g"
@@ -2345,7 +2345,7 @@
     by (metis \<open>open T\<close> continuous_on_subset inj_onI inj_on_subset invariance_of_domain_gen openin_open openin_open_eq)
 qed
 
-lemma%unimportant invariance_of_domain_homeomorphism:
+lemma invariance_of_domain_homeomorphism:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" "inj_on f S"
   obtains g where "homeomorphism S (f ` S) f g"
@@ -2354,14 +2354,14 @@
     by (simp add: assms continuous_on_inverse_open homeomorphism_def)
 qed
 
-corollary%important invariance_of_domain_homeomorphic:
+corollary invariance_of_domain_homeomorphic:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" "inj_on f S"
   shows "S homeomorphic (f ` S)"
   using%unimportant invariance_of_domain_homeomorphism [OF assms]
   by%unimportant (meson homeomorphic_def)
 
-lemma%unimportant continuous_image_subset_interior:
+lemma continuous_image_subset_interior:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "continuous_on S f" "inj_on f S" "DIM('b) \<le> DIM('a)"
   shows "f ` (interior S) \<subseteq> interior(f ` S)"
@@ -2372,13 +2372,13 @@
      apply (auto simp: subset_inj_on interior_subset continuous_on_subset)
   done
 
-lemma%important homeomorphic_interiors_same_dimension:
+lemma homeomorphic_interiors_same_dimension:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   assumes "S homeomorphic T" and dimeq: "DIM('a) = DIM('b)"
   shows "(interior S) homeomorphic (interior T)"
   using assms [unfolded homeomorphic_minimal]
   unfolding homeomorphic_def
-proof%unimportant (clarify elim!: ex_forward)
+proof (clarify elim!: ex_forward)
   fix f g
   assume S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
      and contf: "continuous_on S f" and contg: "continuous_on T g"
@@ -2422,7 +2422,7 @@
   qed
 qed
 
-lemma%unimportant homeomorphic_open_imp_same_dimension:
+lemma homeomorphic_open_imp_same_dimension:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   assumes "S homeomorphic T" "open S" "S \<noteq> {}" "open T" "T \<noteq> {}"
   shows "DIM('a) = DIM('b)"
@@ -2431,7 +2431,7 @@
     apply (rule order_antisym; metis inj_onI invariance_of_dimension)
     done
 
-lemma%unimportant homeomorphic_interiors:
+proposition homeomorphic_interiors:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   assumes "S homeomorphic T" "interior S = {} \<longleftrightarrow> interior T = {}"
     shows "(interior S) homeomorphic (interior T)"
@@ -2449,7 +2449,7 @@
     by (rule homeomorphic_interiors_same_dimension [OF \<open>S homeomorphic T\<close>])
 qed
 
-lemma%unimportant homeomorphic_frontiers_same_dimension:
+lemma homeomorphic_frontiers_same_dimension:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   assumes "S homeomorphic T" "closed S" "closed T" and dimeq: "DIM('a) = DIM('b)"
   shows "(frontier S) homeomorphic (frontier T)"
@@ -2505,7 +2505,7 @@
   qed
 qed
 
-lemma%unimportant homeomorphic_frontiers:
+lemma homeomorphic_frontiers:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   assumes "S homeomorphic T" "closed S" "closed T"
           "interior S = {} \<longleftrightarrow> interior T = {}"
@@ -2522,7 +2522,7 @@
     using False assms homeomorphic_interiors homeomorphic_open_imp_same_dimension by blast
 qed
 
-lemma%unimportant continuous_image_subset_rel_interior:
+lemma continuous_image_subset_rel_interior:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
       and TS: "aff_dim T \<le> aff_dim S"
@@ -2545,7 +2545,7 @@
   qed auto
 qed
 
-lemma%unimportant homeomorphic_rel_interiors_same_dimension:
+lemma homeomorphic_rel_interiors_same_dimension:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T"
   shows "(rel_interior S) homeomorphic (rel_interior T)"
@@ -2597,11 +2597,11 @@
   qed
 qed
 
-lemma%important homeomorphic_rel_interiors:
+lemma homeomorphic_rel_interiors:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   assumes "S homeomorphic T" "rel_interior S = {} \<longleftrightarrow> rel_interior T = {}"
     shows "(rel_interior S) homeomorphic (rel_interior T)"
-proof%unimportant (cases "rel_interior T = {}")
+proof (cases "rel_interior T = {}")
   case True
   with assms show ?thesis by auto
 next
@@ -2630,7 +2630,7 @@
 qed
 
 
-lemma%unimportant homeomorphic_rel_boundaries_same_dimension:
+lemma homeomorphic_rel_boundaries_same_dimension:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T"
   shows "(S - rel_interior S) homeomorphic (T - rel_interior T)"
@@ -2664,7 +2664,7 @@
   qed
 qed
 
-lemma%unimportant homeomorphic_rel_boundaries:
+lemma homeomorphic_rel_boundaries:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   assumes "S homeomorphic T" "rel_interior S = {} \<longleftrightarrow> rel_interior T = {}"
     shows "(S - rel_interior S) homeomorphic (T - rel_interior T)"
@@ -2696,11 +2696,11 @@
     by (rule homeomorphic_rel_boundaries_same_dimension [OF \<open>S homeomorphic T\<close>])
 qed
 
-proposition%important uniformly_continuous_homeomorphism_UNIV_trivial:
+proposition uniformly_continuous_homeomorphism_UNIV_trivial:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
   assumes contf: "uniformly_continuous_on S f" and hom: "homeomorphism S UNIV f g"
   shows "S = UNIV"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
   case True
   then show ?thesis
     by (metis UNIV_I hom empty_iff homeomorphism_def image_eqI)
@@ -2744,7 +2744,7 @@
 
 subsection%important\<open>Dimension-based conditions for various homeomorphisms\<close>
 
-lemma%unimportant homeomorphic_subspaces_eq:
+lemma homeomorphic_subspaces_eq:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   assumes "subspace S" "subspace T"
   shows "S homeomorphic T \<longleftrightarrow> dim S = dim T"
@@ -2765,7 +2765,7 @@
     by (simp add: assms homeomorphic_subspaces)
 qed
 
-lemma%unimportant homeomorphic_affine_sets_eq:
+lemma homeomorphic_affine_sets_eq:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   assumes "affine S" "affine T"
   shows "S homeomorphic T \<longleftrightarrow> aff_dim S = aff_dim T"
@@ -2783,19 +2783,19 @@
     by (metis affine_imp_convex assms homeomorphic_affine_sets homeomorphic_convex_sets)
 qed
 
-lemma%unimportant homeomorphic_hyperplanes_eq:
+lemma homeomorphic_hyperplanes_eq:
   fixes a :: "'a::euclidean_space" and c :: "'b::euclidean_space"
   assumes "a \<noteq> 0" "c \<noteq> 0"
   shows "({x. a \<bullet> x = b} homeomorphic {x. c \<bullet> x = d} \<longleftrightarrow> DIM('a) = DIM('b))"
   apply (auto simp: homeomorphic_affine_sets_eq affine_hyperplane assms)
   by (metis DIM_positive Suc_pred)
 
-lemma%unimportant homeomorphic_UNIV_UNIV:
+lemma homeomorphic_UNIV_UNIV:
   shows "(UNIV::'a set) homeomorphic (UNIV::'b set) \<longleftrightarrow>
     DIM('a::euclidean_space) = DIM('b::euclidean_space)"
   by (simp add: homeomorphic_subspaces_eq)
 
-lemma%unimportant simply_connected_sphere_gen:
+lemma simply_connected_sphere_gen:
    assumes "convex S" "bounded S" and 3: "3 \<le> aff_dim S"
    shows "simply_connected(rel_frontier S)"
 proof -
@@ -2819,16 +2819,16 @@
   qed
 qed
 
-subsection%important\<open>more invariance of domain\<close>
-
-proposition%important invariance_of_domain_sphere_affine_set_gen:
+subsection%important\<open>more invariance of domain\<close>(*FIX ME title? *)
+
+proposition invariance_of_domain_sphere_affine_set_gen:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
       and U: "bounded U" "convex U"
       and "affine T" and affTU: "aff_dim T < aff_dim U"
       and ope: "openin (subtopology euclidean (rel_frontier U)) S"
    shows "openin (subtopology euclidean T) (f ` S)"
-proof%unimportant (cases "rel_frontier U = {}")
+proof (cases "rel_frontier U = {}")
   case True
   then show ?thesis
     using ope openin_subset by force
@@ -2927,7 +2927,7 @@
 qed
 
 
-lemma%unimportant invariance_of_domain_sphere_affine_set:
+lemma invariance_of_domain_sphere_affine_set:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
       and "r \<noteq> 0" "affine T" and affTU: "aff_dim T < DIM('a)"
@@ -2948,7 +2948,7 @@
   qed
 qed
 
-lemma%unimportant no_embedding_sphere_lowdim:
+lemma no_embedding_sphere_lowdim:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes contf: "continuous_on (sphere a r) f" and injf: "inj_on f (sphere a r)" and "r > 0"
    shows "DIM('a) \<le> DIM('b)"
@@ -2969,7 +2969,7 @@
     using not_less by blast
 qed
 
-lemma%unimportant simply_connected_sphere:
+lemma simply_connected_sphere:
   fixes a :: "'a::euclidean_space"
   assumes "3 \<le> DIM('a)"
     shows "simply_connected(sphere a r)"
@@ -2986,7 +2986,7 @@
     by (simp add: aff_dim_cball)
 qed
 
-lemma%unimportant simply_connected_sphere_eq:
+lemma simply_connected_sphere_eq:
   fixes a :: "'a::euclidean_space"
   shows "simply_connected(sphere a r) \<longleftrightarrow> 3 \<le> DIM('a) \<or> r \<le> 0"  (is "?lhs = ?rhs")
 proof (cases "r \<le> 0")
@@ -3029,7 +3029,7 @@
 qed
 
 
-lemma%unimportant simply_connected_punctured_universe_eq:
+lemma simply_connected_punctured_universe_eq:
   fixes a :: "'a::euclidean_space"
   shows "simply_connected(- {a}) \<longleftrightarrow> 3 \<le> DIM('a)"
 proof -
@@ -3047,17 +3047,17 @@
   finally show ?thesis .
 qed
 
-lemma%unimportant not_simply_connected_circle:
+lemma not_simply_connected_circle:
   fixes a :: complex
   shows "0 < r \<Longrightarrow> \<not> simply_connected(sphere a r)"
 by (simp add: simply_connected_sphere_eq)
 
 
-proposition%important simply_connected_punctured_convex:
+proposition simply_connected_punctured_convex:
   fixes a :: "'a::euclidean_space"
   assumes "convex S" and 3: "3 \<le> aff_dim S"
     shows "simply_connected(S - {a})"
-proof%unimportant (cases "a \<in> rel_interior S")
+proof (cases "a \<in> rel_interior S")
   case True
   then obtain e where "a \<in> S" "0 < e" and e: "cball a e \<inter> affine hull S \<subseteq> S"
     by (auto simp: rel_interior_cball)
@@ -3096,11 +3096,11 @@
     by (meson Diff_subset closure_subset subset_trans)
 qed
 
-corollary%important simply_connected_punctured_universe:
+corollary simply_connected_punctured_universe:
   fixes a :: "'a::euclidean_space"
   assumes "3 \<le> DIM('a)"
   shows "simply_connected(- {a})"
-proof%unimportant -
+proof -
   have [simp]: "affine hull cball a 1 = UNIV"
     apply auto
     by (metis UNIV_I aff_dim_cball aff_dim_lt_full zero_less_one not_less_iff_gr_or_eq)
@@ -3116,10 +3116,10 @@
 
 subsection%important\<open>The power, squaring and exponential functions as covering maps\<close>
 
-proposition%important covering_space_power_punctured_plane:
+proposition covering_space_power_punctured_plane:
   assumes "0 < n"
     shows "covering_space (- {0}) (\<lambda>z::complex. z^n) (- {0})"
-proof%unimportant -
+proof -
   consider "n = 1" | "2 \<le> n" using assms by linarith
   then obtain e where "0 < e"
                 and e: "\<And>w z. cmod(w - z) < e * cmod z \<Longrightarrow> (w^n = z^n \<longleftrightarrow> w = z)"
@@ -3367,14 +3367,14 @@
     done
 qed
 
-corollary%important covering_space_square_punctured_plane:
+corollary covering_space_square_punctured_plane:
   "covering_space (- {0}) (\<lambda>z::complex. z^2) (- {0})"
   by%unimportant (simp add: covering_space_power_punctured_plane)
 
 
-proposition%important covering_space_exp_punctured_plane:
+proposition covering_space_exp_punctured_plane:
   "covering_space UNIV (\<lambda>z::complex. exp z) (- {0})"
-proof%unimportant (simp add: covering_space_def, intro conjI ballI)
+proof (simp add: covering_space_def, intro conjI ballI)
   show "continuous_on UNIV (\<lambda>z::complex. exp z)"
     by (rule continuous_on_exp [OF continuous_on_id])
   show "range exp = - {0::complex}"
@@ -3487,9 +3487,9 @@
 qed
 
 
-subsection%important\<open>Hence the Borsukian results about mappings into circles\<close>
-
-lemma%unimportant inessential_eq_continuous_logarithm:
+subsection%important\<open>Hence the Borsukian results about mappings into circles\<close>(*FIX ME title *)
+
+lemma inessential_eq_continuous_logarithm:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
   shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)) \<longleftrightarrow>
          (\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(g x)))"
@@ -3513,7 +3513,7 @@
     by (simp add: f homotopic_with_eq)
 qed
 
-corollary%important inessential_imp_continuous_logarithm_circle:
+corollary inessential_imp_continuous_logarithm_circle:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
   assumes "homotopic_with (\<lambda>h. True) S (sphere 0 1) f (\<lambda>t. a)"
   obtains g where "continuous_on S g" and "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
@@ -3525,7 +3525,7 @@
 qed
 
 
-lemma%unimportant inessential_eq_continuous_logarithm_circle:
+lemma inessential_eq_continuous_logarithm_circle:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
   shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (sphere 0 1) f (\<lambda>t. a)) \<longleftrightarrow>
          (\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(\<i> * of_real(g x))))"
@@ -3565,12 +3565,12 @@
     by (simp add: homotopic_with_eq)
 qed
 
-lemma%important homotopic_with_sphere_times:
+proposition homotopic_with_sphere_times:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
   assumes hom: "homotopic_with (\<lambda>x. True) S (sphere 0 1) f g" and conth: "continuous_on S h"
       and hin: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> sphere 0 1"
     shows "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x * h x) (\<lambda>x. g x * h x)"
-proof%unimportant -
+proof -
   obtain k where contk: "continuous_on ({0..1::real} \<times> S) k"
              and kim: "k ` ({0..1} \<times> S) \<subseteq> sphere 0 1"
              and k0:  "\<And>x. k(0, x) = f x"
@@ -3585,14 +3585,13 @@
     done
 qed
 
-
-lemma%important homotopic_circlemaps_divide:
+proposition homotopic_circlemaps_divide:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
     shows "homotopic_with (\<lambda>x. True) S (sphere 0 1) f g \<longleftrightarrow>
            continuous_on S f \<and> f ` S \<subseteq> sphere 0 1 \<and>
            continuous_on S g \<and> g ` S \<subseteq> sphere 0 1 \<and>
            (\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c))"
-proof%unimportant -
+proof -
   have "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
        if "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c)" for c
   proof -
@@ -3646,7 +3645,7 @@
 
 
 text\<open>Many similar proofs below.\<close>
-lemma%unimportant upper_hemicontinuous:
+lemma upper_hemicontinuous:
   assumes "\<And>x. x \<in> S \<Longrightarrow> f x \<subseteq> T"
     shows "((\<forall>U. openin (subtopology euclidean T) U
                  \<longrightarrow> openin (subtopology euclidean S) {x \<in> S. f x \<subseteq> U}) \<longleftrightarrow>
@@ -3677,7 +3676,7 @@
     by (simp add: openin_closedin_eq)
 qed
 
-lemma%unimportant lower_hemicontinuous:
+lemma lower_hemicontinuous:
   assumes "\<And>x. x \<in> S \<Longrightarrow> f x \<subseteq> T"
     shows "((\<forall>U. closedin (subtopology euclidean T) U
                  \<longrightarrow> closedin (subtopology euclidean S) {x \<in> S. f x \<subseteq> U}) \<longleftrightarrow>
@@ -3708,7 +3707,7 @@
     by (simp add: openin_closedin_eq)
 qed
 
-lemma%unimportant open_map_iff_lower_hemicontinuous_preimage:
+lemma open_map_iff_lower_hemicontinuous_preimage:
   assumes "f ` S \<subseteq> T"
     shows "((\<forall>U. openin (subtopology euclidean S) U
                  \<longrightarrow> openin (subtopology euclidean T) (f ` U)) \<longleftrightarrow>
@@ -3739,7 +3738,7 @@
     using assms openin_imp_subset [OF opeSU] by (force simp: openin_closedin_eq)
 qed
 
-lemma%unimportant closed_map_iff_upper_hemicontinuous_preimage:
+lemma closed_map_iff_upper_hemicontinuous_preimage:
   assumes "f ` S \<subseteq> T"
     shows "((\<forall>U. closedin (subtopology euclidean S) U
                  \<longrightarrow> closedin (subtopology euclidean T) (f ` U)) \<longleftrightarrow>
@@ -3770,7 +3769,7 @@
     by (simp add: openin_closedin_eq)
 qed
 
-proposition%important upper_lower_hemicontinuous_explicit:
+proposition upper_lower_hemicontinuous_explicit:
   fixes T :: "('b::{real_normed_vector,heine_borel}) set"
   assumes fST: "\<And>x. x \<in> S \<Longrightarrow> f x \<subseteq> T"
       and ope: "\<And>U. openin (subtopology euclidean T) U
@@ -3782,7 +3781,7 @@
              "\<And>x'. \<lbrakk>x' \<in> S; dist x x' < d\<rbrakk>
                            \<Longrightarrow> (\<forall>y \<in> f x. \<exists>y'. y' \<in> f x' \<and> dist y y' < e) \<and>
                                (\<forall>y' \<in> f x'. \<exists>y. y \<in> f x \<and> dist y' y < e)"
-proof%unimportant -
+proof -
   have "openin (subtopology euclidean T) (T \<inter> (\<Union>a\<in>f x. \<Union>b\<in>ball 0 e. {a + b}))"
     by (auto simp: open_sums openin_open_Int)
   with ope have "openin (subtopology euclidean S)
@@ -3843,11 +3842,11 @@
 
 subsection%important\<open>Complex logs exist on various "well-behaved" sets\<close>
 
-lemma%important continuous_logarithm_on_contractible:
+lemma continuous_logarithm_on_contractible:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
   assumes "continuous_on S f" "contractible S" "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
   obtains g where "continuous_on S g" "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
-proof%unimportant -
+proof -
   obtain c where hom: "homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>x. c)"
     using nullhomotopic_from_contractible assms
     by (metis imageE subset_Compl_singleton)
@@ -3855,27 +3854,27 @@
     by (metis inessential_eq_continuous_logarithm that)
 qed
 
-lemma%important continuous_logarithm_on_simply_connected:
+lemma continuous_logarithm_on_simply_connected:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
   assumes contf: "continuous_on S f" and S: "simply_connected S" "locally path_connected S"
       and f: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
   obtains g where "continuous_on S g" "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
-  using%unimportant covering_space_lift [OF covering_space_exp_punctured_plane S contf]
-  by%unimportant (metis (full_types) f imageE subset_Compl_singleton)
-
-lemma%unimportant continuous_logarithm_on_cball:
+  using covering_space_lift [OF covering_space_exp_punctured_plane S contf]
+  by (metis (full_types) f imageE subset_Compl_singleton)
+
+lemma continuous_logarithm_on_cball:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
   assumes "continuous_on (cball a r) f" and "\<And>z. z \<in> cball a r \<Longrightarrow> f z \<noteq> 0"
     obtains h where "continuous_on (cball a r) h" "\<And>z. z \<in> cball a r \<Longrightarrow> f z = exp(h z)"
   using assms continuous_logarithm_on_contractible convex_imp_contractible by blast
 
-lemma%unimportant continuous_logarithm_on_ball:
+lemma continuous_logarithm_on_ball:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
   assumes "continuous_on (ball a r) f" and "\<And>z. z \<in> ball a r \<Longrightarrow> f z \<noteq> 0"
   obtains h where "continuous_on (ball a r) h" "\<And>z. z \<in> ball a r \<Longrightarrow> f z = exp(h z)"
   using assms continuous_logarithm_on_contractible convex_imp_contractible by blast
 
-lemma%unimportant continuous_sqrt_on_contractible:
+lemma continuous_sqrt_on_contractible:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
   assumes "continuous_on S f" "contractible S"
       and "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
@@ -3892,7 +3891,7 @@
   qed
 qed
 
-lemma%unimportant continuous_sqrt_on_simply_connected:
+lemma continuous_sqrt_on_simply_connected:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
   assumes contf: "continuous_on S f" and S: "simply_connected S" "locally path_connected S"
       and f: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
@@ -3912,12 +3911,12 @@
 
 subsection%important\<open>Another simple case where sphere maps are nullhomotopic\<close>
 
-lemma%important inessential_spheremap_2_aux:
+lemma inessential_spheremap_2_aux:
   fixes f :: "'a::euclidean_space \<Rightarrow> complex"
   assumes 2: "2 < DIM('a)" and contf: "continuous_on (sphere a r) f" 
       and fim: "f `(sphere a r) \<subseteq> (sphere 0 1)" 
   obtains c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere 0 1) f (\<lambda>x. c)"
-proof%unimportant -
+proof -
   obtain g where contg: "continuous_on (sphere a r) g" 
              and feq: "\<And>x. x \<in> sphere a r \<Longrightarrow> f x = exp(g x)"
   proof (rule continuous_logarithm_on_simply_connected [OF contf])
@@ -3939,12 +3938,12 @@
     by metis
 qed
 
-lemma%important inessential_spheremap_2:
+lemma inessential_spheremap_2:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes a2: "2 < DIM('a)" and b2: "DIM('b) = 2" 
       and contf: "continuous_on (sphere a r) f" and fim: "f `(sphere a r) \<subseteq> (sphere b s)"
   obtains c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. c)"
-proof%unimportant (cases "s \<le> 0")
+proof (cases "s \<le> 0")
   case True
   then show ?thesis
     using contf contractible_sphere fim nullhomotopic_into_contractible that by blast
@@ -3978,12 +3977,12 @@
 
 subsection%important\<open>Holomorphic logarithms and square roots\<close>
 
-lemma%important contractible_imp_holomorphic_log:
+lemma contractible_imp_holomorphic_log:
   assumes holf: "f holomorphic_on S"
       and S: "contractible S"
       and fnz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
   obtains g where "g holomorphic_on S" "\<And>z. z \<in> S \<Longrightarrow> f z = exp(g z)"
-proof%unimportant -
+proof -
   have contf: "continuous_on S f"
     by (simp add: holf holomorphic_on_imp_continuous_on)
   obtain g where contg: "continuous_on S g" and feq: "\<And>x. x \<in> S \<Longrightarrow> f x = exp (g x)"
@@ -4026,12 +4025,12 @@
 qed
 
 (*Identical proofs*)
-lemma%important simply_connected_imp_holomorphic_log:
+lemma simply_connected_imp_holomorphic_log:
   assumes holf: "f holomorphic_on S"
       and S: "simply_connected S" "locally path_connected S"
       and fnz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
   obtains g where "g holomorphic_on S" "\<And>z. z \<in> S \<Longrightarrow> f z = exp(g z)"
-proof%unimportant -
+proof -
   have contf: "continuous_on S f"
     by (simp add: holf holomorphic_on_imp_continuous_on)
   obtain g where contg: "continuous_on S g" and feq: "\<And>x. x \<in> S \<Longrightarrow> f x = exp (g x)"
@@ -4074,7 +4073,7 @@
 qed
 
 
-lemma%unimportant contractible_imp_holomorphic_sqrt:
+lemma contractible_imp_holomorphic_sqrt:
   assumes holf: "f holomorphic_on S"
       and S: "contractible S"
       and fnz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
@@ -4092,7 +4091,7 @@
   qed
 qed
 
-lemma%unimportant simply_connected_imp_holomorphic_sqrt:
+lemma simply_connected_imp_holomorphic_sqrt:
   assumes holf: "f holomorphic_on S"
       and S: "simply_connected S" "locally path_connected S"
       and fnz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
@@ -4112,11 +4111,11 @@
 
 text\<open> Related theorems about holomorphic inverse cosines.\<close>
 
-lemma%important contractible_imp_holomorphic_arccos:
+lemma contractible_imp_holomorphic_arccos:
   assumes holf: "f holomorphic_on S" and S: "contractible S"
       and non1: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 1 \<and> f z \<noteq> -1"
   obtains g where "g holomorphic_on S" "\<And>z. z \<in> S \<Longrightarrow> f z = cos(g z)"
-proof%unimportant -
+proof -
   have hol1f: "(\<lambda>z. 1 - f z ^ 2) holomorphic_on S"
     by (intro holomorphic_intros holf)
   obtain g where holg: "g holomorphic_on S" and eq: "\<And>z. z \<in> S \<Longrightarrow> 1 - (f z)\<^sup>2 = (g z)\<^sup>2"
@@ -4150,11 +4149,11 @@
 qed
 
 
-lemma%important contractible_imp_holomorphic_arccos_bounded:
+lemma contractible_imp_holomorphic_arccos_bounded:
   assumes holf: "f holomorphic_on S" and S: "contractible S" and "a \<in> S"
       and non1: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 1 \<and> f z \<noteq> -1"
   obtains g where "g holomorphic_on S" "norm(g a) \<le> pi + norm(f a)" "\<And>z. z \<in> S \<Longrightarrow> f z = cos(g z)"
-proof%unimportant -
+proof -
   obtain g where holg: "g holomorphic_on S" and feq: "\<And>z. z \<in> S \<Longrightarrow> f z = cos (g z)"
     using contractible_imp_holomorphic_arccos [OF holf S non1] by blast
   obtain b where "cos b = f a" "norm b \<le> pi + norm (f a)"
@@ -4200,11 +4199,11 @@
         \<forall>f. continuous_on S f \<and> f ` S \<subseteq> (- {0::complex})
             \<longrightarrow> (\<exists>a. homotopic_with (\<lambda>h. True) S (- {0}) f (\<lambda>x. a))"
 
-lemma%important Borsukian_retraction_gen:
+lemma Borsukian_retraction_gen:
   assumes "Borsukian S" "continuous_on S h" "h ` S = T"
           "continuous_on T k"  "k ` T \<subseteq> S"  "\<And>y. y \<in> T \<Longrightarrow> h(k y) = y"
     shows "Borsukian T"
-proof%unimportant -
+proof -
   interpret R: Retracts S h T k
     using assms by (simp add: Retracts.intro)
   show ?thesis
@@ -4214,42 +4213,42 @@
     done
 qed
 
-lemma%unimportant retract_of_Borsukian: "\<lbrakk>Borsukian T; S retract_of T\<rbrakk> \<Longrightarrow> Borsukian S"
+lemma retract_of_Borsukian: "\<lbrakk>Borsukian T; S retract_of T\<rbrakk> \<Longrightarrow> Borsukian S"
   apply (auto simp: retract_of_def retraction_def)
   apply (erule (1) Borsukian_retraction_gen)
   apply (meson retraction retraction_def)
     apply (auto simp: continuous_on_id)
     done
 
-lemma%unimportant homeomorphic_Borsukian: "\<lbrakk>Borsukian S; S homeomorphic T\<rbrakk> \<Longrightarrow> Borsukian T"
+lemma homeomorphic_Borsukian: "\<lbrakk>Borsukian S; S homeomorphic T\<rbrakk> \<Longrightarrow> Borsukian T"
   using Borsukian_retraction_gen order_refl
   by (fastforce simp add: homeomorphism_def homeomorphic_def)
 
-lemma%unimportant homeomorphic_Borsukian_eq:
+lemma homeomorphic_Borsukian_eq:
    "S homeomorphic T \<Longrightarrow> Borsukian S \<longleftrightarrow> Borsukian T"
   by (meson homeomorphic_Borsukian homeomorphic_sym)
 
-lemma%unimportant Borsukian_translation:
+lemma Borsukian_translation:
   fixes S :: "'a::real_normed_vector set"
   shows "Borsukian (image (\<lambda>x. a + x) S) \<longleftrightarrow> Borsukian S"
   apply (rule homeomorphic_Borsukian_eq)
     using homeomorphic_translation homeomorphic_sym by blast
 
-lemma%unimportant Borsukian_injective_linear_image:
+lemma Borsukian_injective_linear_image:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "linear f" "inj f"
     shows "Borsukian(f ` S) \<longleftrightarrow> Borsukian S"
   apply (rule homeomorphic_Borsukian_eq)
   using assms homeomorphic_sym linear_homeomorphic_image by blast
 
-lemma%unimportant homotopy_eqv_Borsukianness:
+lemma homotopy_eqv_Borsukianness:
   fixes S :: "'a::real_normed_vector set"
     and T :: "'b::real_normed_vector set"
    assumes "S homotopy_eqv T"
      shows "(Borsukian S \<longleftrightarrow> Borsukian T)"
   by (meson Borsukian_def assms homotopy_eqv_cohomotopic_triviality_null)
 
-lemma%unimportant Borsukian_alt:
+lemma Borsukian_alt:
   fixes S :: "'a::real_normed_vector set"
   shows
    "Borsukian S \<longleftrightarrow>
@@ -4259,20 +4258,20 @@
   unfolding Borsukian_def homotopic_triviality
   by (simp add: path_connected_punctured_universe)
 
-lemma%unimportant Borsukian_continuous_logarithm:
+lemma Borsukian_continuous_logarithm:
   fixes S :: "'a::real_normed_vector set"
   shows "Borsukian S \<longleftrightarrow>
             (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> (- {0::complex})
                  \<longrightarrow> (\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(g x))))"
   by (simp add: Borsukian_def inessential_eq_continuous_logarithm)
 
-lemma%important Borsukian_continuous_logarithm_circle:
+lemma Borsukian_continuous_logarithm_circle:
   fixes S :: "'a::real_normed_vector set"
   shows "Borsukian S \<longleftrightarrow>
              (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::complex) 1
                   \<longrightarrow> (\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(g x))))"
    (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume ?lhs then show ?rhs
     by (force simp: Borsukian_continuous_logarithm)
 next
@@ -4302,13 +4301,13 @@
 qed
 
 
-lemma%important Borsukian_continuous_logarithm_circle_real:
+lemma Borsukian_continuous_logarithm_circle_real:
   fixes S :: "'a::real_normed_vector set"
   shows "Borsukian S \<longleftrightarrow>
          (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::complex) 1
               \<longrightarrow> (\<exists>g. continuous_on S (complex_of_real \<circ> g) \<and> (\<forall>x \<in> S. f x = exp(\<i> * of_real(g x)))))"
    (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume LHS: ?lhs
   show ?rhs
   proof (clarify)
@@ -4335,52 +4334,52 @@
   qed
 qed
 
-lemma%unimportant Borsukian_circle:
+lemma Borsukian_circle:
   fixes S :: "'a::real_normed_vector set"
   shows "Borsukian S \<longleftrightarrow>
          (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::complex) 1
               \<longrightarrow> (\<exists>a. homotopic_with (\<lambda>h. True) S (sphere (0::complex) 1) f (\<lambda>x. a)))"
 by (simp add: inessential_eq_continuous_logarithm_circle Borsukian_continuous_logarithm_circle_real)
 
-lemma%unimportant contractible_imp_Borsukian: "contractible S \<Longrightarrow> Borsukian S"
+lemma contractible_imp_Borsukian: "contractible S \<Longrightarrow> Borsukian S"
   by (meson Borsukian_def nullhomotopic_from_contractible)
 
-lemma%unimportant simply_connected_imp_Borsukian:
+lemma simply_connected_imp_Borsukian:
   fixes S :: "'a::real_normed_vector set"
   shows  "\<lbrakk>simply_connected S; locally path_connected S\<rbrakk> \<Longrightarrow> Borsukian S"
   apply (simp add: Borsukian_continuous_logarithm)
   by (metis (no_types, lifting) continuous_logarithm_on_simply_connected image_iff)
 
-lemma%unimportant starlike_imp_Borsukian:
+lemma starlike_imp_Borsukian:
   fixes S :: "'a::real_normed_vector set"
   shows "starlike S \<Longrightarrow> Borsukian S"
   by (simp add: contractible_imp_Borsukian starlike_imp_contractible)
 
-lemma%unimportant Borsukian_empty: "Borsukian {}"
+lemma Borsukian_empty: "Borsukian {}"
   by (auto simp: contractible_imp_Borsukian)
 
-lemma%unimportant Borsukian_UNIV: "Borsukian (UNIV :: 'a::real_normed_vector set)"
+lemma Borsukian_UNIV: "Borsukian (UNIV :: 'a::real_normed_vector set)"
   by (auto simp: contractible_imp_Borsukian)
 
-lemma%unimportant convex_imp_Borsukian:
+lemma convex_imp_Borsukian:
   fixes S :: "'a::real_normed_vector set"
   shows "convex S \<Longrightarrow> Borsukian S"
   by (meson Borsukian_def convex_imp_contractible nullhomotopic_from_contractible)
 
-lemma%unimportant Borsukian_sphere:
+proposition Borsukian_sphere:
   fixes a :: "'a::euclidean_space"
   shows "3 \<le> DIM('a) \<Longrightarrow> Borsukian (sphere a r)"
   apply (rule simply_connected_imp_Borsukian)
   using simply_connected_sphere apply blast
   using ENR_imp_locally_path_connected ENR_sphere by blast
 
-lemma%important Borsukian_open_Un:
+proposition Borsukian_open_Un:
   fixes S :: "'a::real_normed_vector set"
   assumes opeS: "openin (subtopology euclidean (S \<union> T)) S"
       and opeT: "openin (subtopology euclidean (S \<union> T)) T"
       and BS: "Borsukian S" and BT: "Borsukian T" and ST: "connected(S \<inter> T)"
     shows "Borsukian(S \<union> T)"
-proof%unimportant (clarsimp simp add: Borsukian_continuous_logarithm)
+proof (clarsimp simp add: Borsukian_continuous_logarithm)
   fix f :: "'a \<Rightarrow> complex"
   assume contf: "continuous_on (S \<union> T) f" and 0: "0 \<notin> f ` (S \<union> T)"
   then have contfS: "continuous_on S f" and contfT: "continuous_on T f"
@@ -4444,13 +4443,13 @@
 qed
 
 text\<open>The proof is a duplicate of that of \<open>Borsukian_open_Un\<close>.\<close>
-lemma%important Borsukian_closed_Un:
+lemma Borsukian_closed_Un:
   fixes S :: "'a::real_normed_vector set"
   assumes cloS: "closedin (subtopology euclidean (S \<union> T)) S"
       and cloT: "closedin (subtopology euclidean (S \<union> T)) T"
       and BS: "Borsukian S" and BT: "Borsukian T" and ST: "connected(S \<inter> T)"
     shows "Borsukian(S \<union> T)"
-proof%unimportant (clarsimp simp add: Borsukian_continuous_logarithm)
+proof (clarsimp simp add: Borsukian_continuous_logarithm)
   fix f :: "'a \<Rightarrow> complex"
   assume contf: "continuous_on (S \<union> T) f" and 0: "0 \<notin> f ` (S \<union> T)"
   then have contfS: "continuous_on S f" and contfT: "continuous_on T f"
@@ -4513,18 +4512,18 @@
   qed
 qed
 
-lemma%unimportant Borsukian_separation_compact:
+lemma Borsukian_separation_compact:
   fixes S :: "complex set"
   assumes "compact S"
     shows "Borsukian S \<longleftrightarrow> connected(- S)"
   by (simp add: Borsuk_separation_theorem Borsukian_circle assms)
 
-lemma%important Borsukian_monotone_image_compact:
+lemma Borsukian_monotone_image_compact:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "Borsukian S" and contf: "continuous_on S f" and fim: "f ` S = T"
       and "compact S" and conn: "\<And>y. y \<in> T \<Longrightarrow> connected {x. x \<in> S \<and> f x = y}"
     shows "Borsukian T"
-proof%unimportant (clarsimp simp add: Borsukian_continuous_logarithm)
+proof (clarsimp simp add: Borsukian_continuous_logarithm)
   fix g :: "'b \<Rightarrow> complex"
   assume contg: "continuous_on T g" and 0: "0 \<notin> g ` T"
   have "continuous_on S (g \<circ> f)"
@@ -4584,13 +4583,13 @@
 qed
 
 
-lemma%important Borsukian_open_map_image_compact:
+lemma Borsukian_open_map_image_compact:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "Borsukian S" and contf: "continuous_on S f" and fim: "f ` S = T" and "compact S"
       and ope: "\<And>U. openin (subtopology euclidean S) U
                      \<Longrightarrow> openin (subtopology euclidean T) (f ` U)"
     shows "Borsukian T"
-proof%unimportant (clarsimp simp add: Borsukian_continuous_logarithm_circle_real)
+proof (clarsimp simp add: Borsukian_continuous_logarithm_circle_real)
   fix g :: "'b \<Rightarrow> complex"
   assume contg: "continuous_on T g" and gim: "g ` T \<subseteq> sphere 0 1"
   have "continuous_on S (g \<circ> f)"
@@ -4671,12 +4670,12 @@
 
 
 text\<open>If two points are separated by a closed set, there's a minimal one.\<close>
-proposition%important closed_irreducible_separator:
+proposition closed_irreducible_separator:
   fixes a :: "'a::real_normed_vector"
   assumes "closed S" and ab: "\<not> connected_component (- S) a b"
   obtains T where "T \<subseteq> S" "closed T" "T \<noteq> {}" "\<not> connected_component (- T) a b"
                   "\<And>U. U \<subset> T \<Longrightarrow> connected_component (- U) a b"
-proof%unimportant (cases "a \<in> S \<or> b \<in> S")
+proof (cases "a \<in> S \<or> b \<in> S")
   case True
   then show ?thesis
   proof
@@ -4779,7 +4778,7 @@
   qed
 qed
 
-lemma%unimportant frontier_minimal_separating_closed_pointwise:
+lemma frontier_minimal_separating_closed_pointwise:
   fixes S :: "'a::real_normed_vector set"
   assumes S: "closed S" "a \<notin> S" and nconn: "\<not> connected_component (- S) a b"
       and conn: "\<And>T. \<lbrakk>closed T; T \<subset> S\<rbrakk> \<Longrightarrow> connected_component (- T) a b"
@@ -4816,21 +4815,21 @@
         closedin (subtopology euclidean U) S \<and> closedin (subtopology euclidean U) T
         \<longrightarrow> connected (S \<inter> T)"
 
-lemma%unimportant unicoherentI [intro?]:
+lemma unicoherentI [intro?]:
   assumes "\<And>S T. \<lbrakk>connected S; connected T; U = S \<union> T; closedin (subtopology euclidean U) S; closedin (subtopology euclidean U) T\<rbrakk>
           \<Longrightarrow> connected (S \<inter> T)"
   shows "unicoherent U"
   using assms unfolding unicoherent_def by blast
 
-lemma%unimportant unicoherentD:
+lemma unicoherentD:
   assumes "unicoherent U" "connected S" "connected T" "U = S \<union> T" "closedin (subtopology euclidean U) S" "closedin (subtopology euclidean U) T"
   shows "connected (S \<inter> T)"
   using assms unfolding unicoherent_def by blast
 
-lemma%important homeomorphic_unicoherent:
+proposition homeomorphic_unicoherent:
   assumes ST: "S homeomorphic T" and S: "unicoherent S"
   shows "unicoherent T"
-proof%unimportant -
+proof -
   obtain f g where gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x" and fim: "T = f ` S" and gfim: "g ` f ` S = S"
     and contf: "continuous_on S f" and contg: "continuous_on (f ` S) g"
     using ST by (auto simp: homeomorphic_def homeomorphism_def)
@@ -4871,24 +4870,24 @@
 qed
 
 
-lemma%unimportant homeomorphic_unicoherent_eq:
+lemma homeomorphic_unicoherent_eq:
    "S homeomorphic T \<Longrightarrow> (unicoherent S \<longleftrightarrow> unicoherent T)"
   by (meson homeomorphic_sym homeomorphic_unicoherent)
 
-lemma%unimportant unicoherent_translation:
+lemma unicoherent_translation:
   fixes S :: "'a::real_normed_vector set"
   shows
    "unicoherent (image (\<lambda>x. a + x) S) \<longleftrightarrow> unicoherent S"
   using homeomorphic_translation homeomorphic_unicoherent_eq by blast
 
-lemma%unimportant unicoherent_injective_linear_image:
+lemma unicoherent_injective_linear_image:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "linear f" "inj f"
   shows "(unicoherent(f ` S) \<longleftrightarrow> unicoherent S)"
   using assms homeomorphic_unicoherent_eq linear_homeomorphic_image by blast
 
 
-lemma%unimportant Borsukian_imp_unicoherent:
+lemma Borsukian_imp_unicoherent:
   fixes U :: "'a::euclidean_space set"
   assumes "Borsukian U"  shows "unicoherent U"
   unfolding unicoherent_def
@@ -4998,27 +4997,27 @@
 qed
 
 
-corollary%important contractible_imp_unicoherent:
+corollary contractible_imp_unicoherent:
   fixes U :: "'a::euclidean_space set"
   assumes "contractible U"  shows "unicoherent U"
   by%unimportant (simp add: Borsukian_imp_unicoherent assms contractible_imp_Borsukian)
 
-corollary%important convex_imp_unicoherent:
+corollary convex_imp_unicoherent:
   fixes U :: "'a::euclidean_space set"
   assumes "convex U"  shows "unicoherent U"
   by%unimportant (simp add: Borsukian_imp_unicoherent assms convex_imp_Borsukian)
 
 text\<open>If the type class constraint can be relaxed, I don't know how!\<close>
-corollary%important unicoherent_UNIV: "unicoherent (UNIV :: 'a :: euclidean_space set)"
+corollary unicoherent_UNIV: "unicoherent (UNIV :: 'a :: euclidean_space set)"
   by%unimportant (simp add: convex_imp_unicoherent)
 
 
-lemma%important unicoherent_monotone_image_compact:
+lemma unicoherent_monotone_image_compact:
   fixes T :: "'b :: t2_space set"
   assumes S: "unicoherent S" "compact S" and contf: "continuous_on S f" and fim: "f ` S = T"
   and conn: "\<And>y. y \<in> T \<Longrightarrow> connected (S \<inter> f -` {y})"
   shows "unicoherent T"
-proof%unimportant
+proof
   fix U V
   assume UV: "connected U" "connected V" "T = U \<union> V"
      and cloU: "closedin (subtopology euclidean T) U"
@@ -5054,7 +5053,7 @@
 
 subsection%important\<open>Several common variants of unicoherence\<close>
 
-lemma%unimportant connected_frontier_simple:
+lemma connected_frontier_simple:
   fixes S :: "'a :: euclidean_space set"
   assumes "connected S" "connected(- S)" shows "connected(frontier S)"
   unfolding frontier_closures
@@ -5062,18 +5061,18 @@
       apply (simp_all add: assms connected_imp_connected_closure)
   by (simp add: closure_def)
 
-lemma%unimportant connected_frontier_component_complement:
+lemma connected_frontier_component_complement:
   fixes S :: "'a :: euclidean_space set"
   assumes "connected S" and C: "C \<in> components(- S)" shows "connected(frontier C)"
   apply (rule connected_frontier_simple)
   using C in_components_connected apply blast
   by (metis Compl_eq_Diff_UNIV connected_UNIV assms top_greatest component_complement_connected)
 
-lemma%important connected_frontier_disjoint:
+lemma connected_frontier_disjoint:
   fixes S :: "'a :: euclidean_space set"
   assumes "connected S" "connected T" "disjnt S T" and ST: "frontier S \<subseteq> frontier T"
   shows "connected(frontier S)"
-proof%unimportant (cases "S = UNIV")
+proof (cases "S = UNIV")
   case True then show ?thesis
     by simp
 next
@@ -5107,11 +5106,11 @@
 
 subsection%important\<open>Some separation results\<close>
 
-lemma%important separation_by_component_closed_pointwise:
+lemma separation_by_component_closed_pointwise:
   fixes S :: "'a :: euclidean_space set"
   assumes "closed S" "\<not> connected_component (- S) a b"
   obtains C where "C \<in> components S" "\<not> connected_component(- C) a b"
-proof%unimportant (cases "a \<in> S \<or> b \<in> S")
+proof (cases "a \<in> S \<or> b \<in> S")
   case True
   then show ?thesis
     using connected_component_in componentsI that by fastforce
@@ -5144,11 +5143,11 @@
 qed
 
 
-lemma%important separation_by_component_closed:
+lemma separation_by_component_closed:
   fixes S :: "'a :: euclidean_space set"
   assumes "closed S" "\<not> connected(- S)"
   obtains C where "C \<in> components S" "\<not> connected(- C)"
-proof%unimportant -
+proof -
   obtain x y where "closed S" "x \<notin> S" "y \<notin> S" and "\<not> connected_component (- S) x y"
     using assms by (auto simp: connected_iff_connected_component)
   then obtain C where "C \<in> components S" "\<not> connected_component(- C) x y"
@@ -5158,12 +5157,12 @@
     by (metis Compl_iff \<open>C \<in> components S\<close> \<open>x \<notin> S\<close> \<open>y \<notin> S\<close> connected_component_eq connected_component_eq_eq connected_iff_connected_component that)
 qed
 
-lemma%important separation_by_Un_closed_pointwise:
+lemma separation_by_Un_closed_pointwise:
   fixes S :: "'a :: euclidean_space set"
   assumes ST: "closed S" "closed T" "S \<inter> T = {}"
       and conS: "connected_component (- S) a b" and conT: "connected_component (- T) a b"
     shows "connected_component (- (S \<union> T)) a b"
-proof%unimportant (rule ccontr)
+proof (rule ccontr)
   have "a \<notin> S" "b \<notin> S" "a \<notin> T" "b \<notin> T"
     using conS conT connected_component_in by auto
   assume "\<not> connected_component (- (S \<union> T)) a b"
@@ -5182,14 +5181,14 @@
     by (meson Compl_anti_mono C conS conT connected_component_of_subset)
 qed
 
-lemma%unimportant separation_by_Un_closed:
+lemma separation_by_Un_closed:
   fixes S :: "'a :: euclidean_space set"
   assumes ST: "closed S" "closed T" "S \<inter> T = {}" and conS: "connected(- S)" and conT: "connected(- T)"
   shows "connected(- (S \<union> T))"
   using assms separation_by_Un_closed_pointwise
   by (fastforce simp add: connected_iff_connected_component)
 
-lemma%unimportant open_unicoherent_UNIV:
+lemma open_unicoherent_UNIV:
   fixes S :: "'a :: euclidean_space set"
   assumes "open S" "open T" "connected S" "connected T" "S \<union> T = UNIV"
   shows "connected(S \<inter> T)"
@@ -5200,7 +5199,7 @@
     by simp
 qed
 
-lemma%unimportant separation_by_component_open_aux:
+lemma separation_by_component_open_aux:
   fixes S :: "'a :: euclidean_space set"
   assumes ST: "closed S" "closed T" "S \<inter> T = {}"
       and "S \<noteq> {}" "T \<noteq> {}"
@@ -5280,11 +5279,11 @@
 qed
 
 
-lemma%important separation_by_component_open:
+proposition separation_by_component_open:
   fixes S :: "'a :: euclidean_space set"
   assumes "open S" and non: "\<not> connected(- S)"
   obtains C where "C \<in> components S" "\<not> connected(- C)"
-proof%unimportant -
+proof -
   obtain T U
     where "closed T" "closed U" and TU: "T \<union> U = - S" "T \<inter> U = {}" "T \<noteq> {}" "U \<noteq> {}"
     using assms by (auto simp: connected_closed_set closed_def)
@@ -5307,18 +5306,18 @@
   qed
 qed
 
-lemma%unimportant separation_by_Un_open:
+lemma separation_by_Un_open:
   fixes S :: "'a :: euclidean_space set"
   assumes "open S" "open T" "S \<inter> T = {}" and cS: "connected(-S)" and cT: "connected(-T)"
     shows "connected(- (S \<union> T))"
   using assms unicoherent_UNIV unfolding unicoherent_def by force
 
 
-lemma%important nonseparation_by_component_eq:
+lemma nonseparation_by_component_eq:
   fixes S :: "'a :: euclidean_space set"
   assumes "open S \<or> closed S"
   shows "((\<forall>C \<in> components S. connected(-C)) \<longleftrightarrow> connected(- S))" (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume ?lhs with assms show ?rhs
     by (meson separation_by_component_closed separation_by_component_open)
 next
@@ -5328,13 +5327,13 @@
 
 
 text\<open>Another interesting equivalent of an inessential mapping into C-{0}\<close>
-proposition%important inessential_eq_extensible:
+proposition inessential_eq_extensible:
   fixes f :: "'a::euclidean_space \<Rightarrow> complex"
   assumes "closed S"
   shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)) \<longleftrightarrow>
          (\<exists>g. continuous_on UNIV g \<and> (\<forall>x \<in> S. g x = f x) \<and> (\<forall>x. g x \<noteq> 0))"
      (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume ?lhs
   then obtain a where a: "homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)" ..
   show ?rhs
@@ -5394,14 +5393,14 @@
     by (simp add: inessential_eq_continuous_logarithm)
 qed
 
-lemma%important inessential_on_clopen_Union:
+lemma inessential_on_clopen_Union:
   fixes \<F> :: "'a::euclidean_space set set"
   assumes T: "path_connected T"
       and "\<And>S. S \<in> \<F> \<Longrightarrow> closedin (subtopology euclidean (\<Union>\<F>)) S"
       and "\<And>S. S \<in> \<F> \<Longrightarrow> openin (subtopology euclidean (\<Union>\<F>)) S"
       and hom: "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a. homotopic_with (\<lambda>x. True) S T f (\<lambda>x. a)"
   obtains a where "homotopic_with (\<lambda>x. True) (\<Union>\<F>) T f (\<lambda>x. a)"
-proof%unimportant (cases "\<Union>\<F> = {}")
+proof (cases "\<Union>\<F> = {}")
   case True
   with that show ?thesis
     by force
@@ -5442,12 +5441,12 @@
   then show ?thesis ..
 qed
 
-lemma%important Janiszewski_dual:
+proposition Janiszewski_dual:
   fixes S :: "complex set"
   assumes
    "compact S" "compact T" "connected S" "connected T" "connected(- (S \<union> T))"
  shows "connected(S \<inter> T)"
-proof%unimportant -
+proof -
   have ST: "compact (S \<union> T)"
     by (simp add: assms compact_Un)
   with Borsukian_imp_unicoherent [of "S \<union> T"] ST assms
--- a/src/HOL/Analysis/Great_Picard.thy	Wed Jan 16 21:27:33 2019 +0000
+++ b/src/HOL/Analysis/Great_Picard.thy	Thu Jan 17 15:50:28 2019 +0000
@@ -9,13 +9,13 @@
   
 subsection\<open>Schottky's theorem\<close>
 
-lemma%important Schottky_lemma0:
+lemma Schottky_lemma0:
   assumes holf: "f holomorphic_on S" and cons: "contractible S" and "a \<in> S"
       and f: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 1 \<and> f z \<noteq> -1"
   obtains g where "g holomorphic_on S"
                   "norm(g a) \<le> 1 + norm(f a) / 3"
                   "\<And>z. z \<in> S \<Longrightarrow> f z = cos(of_real pi * g z)"
-proof%unimportant -
+proof -
   obtain g where holg: "g holomorphic_on S" and g: "norm(g a) \<le> pi + norm(f a)"
              and f_eq_cos: "\<And>z. z \<in> S \<Longrightarrow> f z = cos(g z)"
     using contractible_imp_holomorphic_arccos_bounded [OF assms]
@@ -38,7 +38,7 @@
 qed
 
 
-lemma%unimportant Schottky_lemma1:
+lemma Schottky_lemma1:
   fixes n::nat
   assumes "0 < n"
   shows "0 < n + sqrt(real n ^ 2 - 1)"
@@ -54,7 +54,7 @@
 qed
 
 
-lemma%unimportant Schottky_lemma2:
+lemma Schottky_lemma2:
   fixes x::real
   assumes "0 \<le> x"
   obtains n where "0 < n" "\<bar>x - ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi\<bar> < 1/2"
@@ -158,12 +158,12 @@
 qed
 
 
-lemma%important Schottky_lemma3:
+lemma Schottky_lemma3:
   fixes z::complex
   assumes "z \<in> (\<Union>m \<in> Ints. \<Union>n \<in> {0<..}. {Complex m (ln(n + sqrt(real n ^ 2 - 1)) / pi)})
              \<union> (\<Union>m \<in> Ints. \<Union>n \<in> {0<..}. {Complex m (-ln(n + sqrt(real n ^ 2 - 1)) / pi)})"
   shows "cos(pi * cos(pi * z)) = 1 \<or> cos(pi * cos(pi * z)) = -1"
-proof%unimportant -
+proof -
   have sqrt2 [simp]: "complex_of_real (sqrt x) * complex_of_real (sqrt x) = x" if "x \<ge> 0" for x::real
     by (metis abs_of_nonneg of_real_mult real_sqrt_mult_self that)
   have 1: "\<exists>k. exp (\<i> * (of_int m * complex_of_real pi) -
@@ -223,13 +223,13 @@
 qed
 
 
-theorem%important Schottky:
+theorem Schottky:
   assumes holf: "f holomorphic_on cball 0 1"
       and nof0: "norm(f 0) \<le> r"
       and not01: "\<And>z. z \<in> cball 0 1 \<Longrightarrow> \<not>(f z = 0 \<or> f z = 1)"
       and "0 < t" "t < 1" "norm z \<le> t"
     shows "norm(f z) \<le> exp(pi * exp(pi * (2 + 2 * r + 12 * t / (1 - t))))"
-proof%unimportant -
+proof -
   obtain h where holf: "h holomorphic_on cball 0 1"
              and nh0: "norm (h 0) \<le> 1 + norm(2 * f 0 - 1) / 3"
              and h:   "\<And>z. z \<in> cball 0 1 \<Longrightarrow> 2 * f z - 1 = cos(of_real pi * h z)"
@@ -376,12 +376,12 @@
   
 subsection%important\<open>The Little Picard Theorem\<close>
 
-lemma%important Landau_Picard:
+proposition Landau_Picard:
   obtains R
     where "\<And>z. 0 < R z"
           "\<And>f. \<lbrakk>f holomorphic_on cball 0 (R(f 0));
                  \<And>z. norm z \<le> R(f 0) \<Longrightarrow> f z \<noteq> 0 \<and> f z \<noteq> 1\<rbrakk> \<Longrightarrow> norm(deriv f 0) < 1"
-proof%unimportant -
+proof -
   define R where "R \<equiv> \<lambda>z. 3 * exp(pi * exp(pi*(2 + 2 * cmod z + 12)))"
   show ?thesis
   proof
@@ -436,10 +436,10 @@
   qed
 qed
 
-lemma%important little_Picard_01:
+lemma little_Picard_01:
   assumes holf: "f holomorphic_on UNIV" and f01: "\<And>z. f z \<noteq> 0 \<and> f z \<noteq> 1"
   obtains c where "f = (\<lambda>x. c)"
-proof%unimportant -
+proof -
   obtain R
     where Rpos: "\<And>z. 0 < R z"
       and R:    "\<And>h. \<lbrakk>h holomorphic_on cball 0 (R(h 0));
@@ -481,11 +481,11 @@
 qed
 
 
-theorem%important little_Picard:
+theorem little_Picard:
   assumes holf: "f holomorphic_on UNIV"
       and "a \<noteq> b" "range f \<inter> {a,b} = {}"
     obtains c where "f = (\<lambda>x. c)"
-proof%unimportant -
+proof -
   let ?g = "\<lambda>x. 1/(b - a)*(f x - b) + 1"
   obtain c where "?g = (\<lambda>x. c)"
   proof (rule little_Picard_01)
@@ -505,7 +505,7 @@
 
 text\<open>A couple of little applications of Little Picard\<close>
 
-lemma%unimportant holomorphic_periodic_fixpoint:
+lemma holomorphic_periodic_fixpoint:
   assumes holf: "f holomorphic_on UNIV"
       and "p \<noteq> 0" and per: "\<And>z. f(z + p) = f z"
   obtains x where "f x = x"
@@ -527,7 +527,7 @@
 qed
 
 
-lemma%unimportant holomorphic_involution_point:
+lemma holomorphic_involution_point:
   assumes holfU: "f holomorphic_on UNIV" and non: "\<And>a. f \<noteq> (\<lambda>x. a + x)"
   obtains x where "f(f x) = x"
 proof -
@@ -616,7 +616,7 @@
 
 subsection%important\<open>The ArzelĂ --Ascoli theorem\<close>
 
-lemma%unimportant subsequence_diagonalization_lemma:
+lemma subsequence_diagonalization_lemma:
   fixes P :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"
   assumes sub: "\<And>i r. \<exists>k. strict_mono (k :: nat \<Rightarrow> nat) \<and> P i (r \<circ> k)"
       and P_P:  "\<And>i r::nat \<Rightarrow> 'a. \<And>k1 k2 N.
@@ -660,7 +660,7 @@
   qed
 qed
 
-lemma%unimportant function_convergent_subsequence:
+lemma function_convergent_subsequence:
   fixes f :: "[nat,'a] \<Rightarrow> 'b::{real_normed_vector,heine_borel}"
   assumes "countable S" and M: "\<And>n::nat. \<And>x. x \<in> S \<Longrightarrow> norm(f n x) \<le> M"
    obtains k where "strict_mono (k::nat\<Rightarrow>nat)" "\<And>x. x \<in> S \<Longrightarrow> \<exists>l. (\<lambda>n. f (k n) x) \<longlonglongrightarrow> l"
@@ -698,7 +698,7 @@
 qed
 
 
-theorem%important Arzela_Ascoli:
+theorem Arzela_Ascoli:
   fixes \<F> :: "[nat,'a::euclidean_space] \<Rightarrow> 'b::{real_normed_vector,heine_borel}"
   assumes "compact S"
       and M: "\<And>n x. x \<in> S \<Longrightarrow> norm(\<F> n x) \<le> M"
@@ -707,7 +707,7 @@
                  \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>n y. y \<in> S \<and> norm(x - y) < d \<longrightarrow> norm(\<F> n x - \<F> n y) < e)"
   obtains g k where "continuous_on S g" "strict_mono (k :: nat \<Rightarrow> nat)"
                     "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. n \<ge> N \<and> x \<in> S \<longrightarrow> norm(\<F>(k n) x - g x) < e"
-proof%unimportant -
+proof -
   have UEQ: "\<And>e. 0 < e \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>n. \<forall>x \<in> S. \<forall>x' \<in> S. dist x' x < d \<longrightarrow> dist (\<F> n x') (\<F> n x) < e)"
     apply (rule compact_uniformly_equicontinuous [OF \<open>compact S\<close>, of "range \<F>"])
     using equicont by (force simp: dist_commute dist_norm)+
@@ -795,7 +795,7 @@
 holomorphic function, and converges \emph{uniformly} on compact subsets of S.\<close>
 
 
-theorem%important Montel:
+theorem Montel:
   fixes \<F> :: "[nat,complex] \<Rightarrow> complex"
   assumes "open S"
       and \<H>: "\<And>h. h \<in> \<H> \<Longrightarrow> h holomorphic_on S"
@@ -805,7 +805,7 @@
     where "g holomorphic_on S" "strict_mono (r :: nat \<Rightarrow> nat)"
           "\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>n. \<F> (r n) x) \<longlongrightarrow> g x) sequentially"
           "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K (\<F> \<circ> r) g sequentially"        
-proof%unimportant -
+proof -
   obtain K where comK: "\<And>n. compact(K n)" and KS: "\<And>n::nat. K n \<subseteq> S"
              and subK: "\<And>X. \<lbrakk>compact X; X \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. X \<subseteq> K n"
     using open_Union_compact_subsets [OF \<open>open S\<close>] by metis
@@ -995,7 +995,7 @@
 
 subsection%important\<open>Some simple but useful cases of Hurwitz's theorem\<close>
 
-proposition%important Hurwitz_no_zeros:
+proposition Hurwitz_no_zeros:
   assumes S: "open S" "connected S"
       and holf: "\<And>n::nat. \<F> n holomorphic_on S"
       and holg: "g holomorphic_on S"
@@ -1004,7 +1004,7 @@
       and nz: "\<And>n z. z \<in> S \<Longrightarrow> \<F> n z \<noteq> 0"
       and "z0 \<in> S"
       shows "g z0 \<noteq> 0"
-proof%unimportant
+proof
   assume g0: "g z0 = 0"
   obtain h r m
     where "0 < m" "0 < r" and subS: "ball z0 r \<subseteq> S"
@@ -1159,7 +1159,7 @@
   ultimately show False using \<open>0 < m\<close> by auto
 qed
 
-corollary%important Hurwitz_injective:
+corollary Hurwitz_injective:
   assumes S: "open S" "connected S"
       and holf: "\<And>n::nat. \<F> n holomorphic_on S"
       and holg: "g holomorphic_on S"
@@ -1167,7 +1167,7 @@
       and nonconst: "\<not> g constant_on S"
       and inj: "\<And>n. inj_on (\<F> n) S"
     shows "inj_on g S"
-proof%unimportant -
+proof -
   have False if z12: "z1 \<in> S" "z2 \<in> S" "z1 \<noteq> z2" "g z2 = g z1" for z1 z2
   proof -
     obtain z0 where "z0 \<in> S" and z0: "g z0 \<noteq> g z2"
@@ -1231,13 +1231,13 @@
 
 subsection%important\<open>The Great Picard theorem\<close>
 
-lemma%important GPicard1:
+lemma GPicard1:
   assumes S: "open S" "connected S" and "w \<in> S" "0 < r" "Y \<subseteq> X"
       and holX: "\<And>h. h \<in> X \<Longrightarrow> h holomorphic_on S"
       and X01:  "\<And>h z. \<lbrakk>h \<in> X; z \<in> S\<rbrakk> \<Longrightarrow> h z \<noteq> 0 \<and> h z \<noteq> 1"
       and r:    "\<And>h. h \<in> Y \<Longrightarrow> norm(h w) \<le> r"
   obtains B Z where "0 < B" "open Z" "w \<in> Z" "Z \<subseteq> S" "\<And>h z. \<lbrakk>h \<in> Y; z \<in> Z\<rbrakk> \<Longrightarrow> norm(h z) \<le> B"
-proof%unimportant -
+proof -
   obtain e where "e > 0" and e: "cball w e \<subseteq> S"
     using assms open_contains_cball_eq by blast
   show ?thesis
@@ -1277,20 +1277,20 @@
   qed (use \<open>e > 0\<close> in auto)
 qed 
 
-lemma%important GPicard2:
+lemma GPicard2:
   assumes "S \<subseteq> T" "connected T" "S \<noteq> {}" "open S" "\<And>x. \<lbrakk>x islimpt S; x \<in> T\<rbrakk> \<Longrightarrow> x \<in> S"
     shows "S = T"
-  by%unimportant (metis assms open_subset connected_clopen closedin_limpt)
+  by (metis assms open_subset connected_clopen closedin_limpt)
 
     
-lemma%important GPicard3:
+lemma GPicard3:
   assumes S: "open S" "connected S" "w \<in> S" and "Y \<subseteq> X"
       and holX: "\<And>h. h \<in> X \<Longrightarrow> h holomorphic_on S"
       and X01:  "\<And>h z. \<lbrakk>h \<in> X; z \<in> S\<rbrakk> \<Longrightarrow> h z \<noteq> 0 \<and> h z \<noteq> 1"
       and no_hw_le1: "\<And>h. h \<in> Y \<Longrightarrow> norm(h w) \<le> 1"
       and "compact K" "K \<subseteq> S"
   obtains B where "\<And>h z. \<lbrakk>h \<in> Y; z \<in> K\<rbrakk> \<Longrightarrow> norm(h z) \<le> B"
-proof%unimportant -
+proof -
   define U where "U \<equiv> {z \<in> S. \<exists>B Z. 0 < B \<and> open Z \<and> z \<in> Z \<and> Z \<subseteq> S \<and>
                                (\<forall>h z'. h \<in> Y \<and> z' \<in> Z \<longrightarrow> norm(h z') \<le> B)}"
   then have "U \<subseteq> S" by blast
@@ -1432,11 +1432,11 @@
 qed
 
 
-lemma%important GPicard4:
+lemma GPicard4:
   assumes "0 < k" and holf: "f holomorphic_on (ball 0 k - {0})" 
       and AE: "\<And>e. \<lbrakk>0 < e; e < k\<rbrakk> \<Longrightarrow> \<exists>d. 0 < d \<and> d < e \<and> (\<forall>z \<in> sphere 0 d. norm(f z) \<le> B)"
   obtains \<epsilon> where "0 < \<epsilon>" "\<epsilon> < k" "\<And>z. z \<in> ball 0 \<epsilon> - {0} \<Longrightarrow> norm(f z) \<le> B"
-proof%unimportant -
+proof -
   obtain \<epsilon> where "0 < \<epsilon>" "\<epsilon> < k/2" and \<epsilon>: "\<And>z. norm z = \<epsilon> \<Longrightarrow> norm(f z) \<le> B"
     using AE [of "k/2"] \<open>0 < k\<close> by auto
   show ?thesis
@@ -1471,13 +1471,13 @@
 qed
   
 
-lemma%important GPicard5:
+lemma GPicard5:
   assumes holf: "f holomorphic_on (ball 0 1 - {0})"
       and f01:  "\<And>z. z \<in> ball 0 1 - {0} \<Longrightarrow> f z \<noteq> 0 \<and> f z \<noteq> 1"
   obtains e B where "0 < e" "e < 1" "0 < B" 
                     "(\<forall>z \<in> ball 0 e - {0}. norm(f z) \<le> B) \<or>
                      (\<forall>z \<in> ball 0 e - {0}. norm(f z) \<ge> B)"
-proof%unimportant -
+proof -
   have [simp]: "1 + of_nat n \<noteq> (0::complex)" for n
     using of_nat_eq_0_iff by fastforce
   have [simp]: "cmod (1 + of_nat n) = 1 + of_nat n" for n
@@ -1614,13 +1614,13 @@
 qed
 
   
-lemma%important GPicard6:
+lemma GPicard6:
   assumes "open M" "z \<in> M" "a \<noteq> 0" and holf: "f holomorphic_on (M - {z})"
       and f0a: "\<And>w. w \<in> M - {z} \<Longrightarrow> f w \<noteq> 0 \<and> f w \<noteq> a"
   obtains r where "0 < r" "ball z r \<subseteq> M" 
                   "bounded(f ` (ball z r - {z})) \<or>
                    bounded((inverse \<circ> f) ` (ball z r - {z}))"
-proof%unimportant -
+proof -
   obtain r where "0 < r" and r: "ball z r \<subseteq> M"
     using assms openE by blast 
   let ?g = "\<lambda>w. f (z + of_real r * w) / a"
@@ -1669,11 +1669,11 @@
 qed
   
 
-theorem%important great_Picard:
+theorem great_Picard:
   assumes "open M" "z \<in> M" "a \<noteq> b" and holf: "f holomorphic_on (M - {z})"
       and fab: "\<And>w. w \<in> M - {z} \<Longrightarrow> f w \<noteq> a \<and> f w \<noteq> b"
   obtains l where "(f \<longlongrightarrow> l) (at z) \<or> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)"
-proof%unimportant -
+proof -
   obtain r where "0 < r" and zrM: "ball z r \<subseteq> M" 
              and r: "bounded((\<lambda>z. f z - a) ` (ball z r - {z})) \<or>
                      bounded((inverse \<circ> (\<lambda>z. f z - a)) ` (ball z r - {z}))"
@@ -1776,7 +1776,7 @@
 qed
 
 
-corollary%important great_Picard_alt:
+corollary great_Picard_alt:
   assumes M: "open M" "z \<in> M" and holf: "f holomorphic_on (M - {z})"
     and non: "\<And>l. \<not> (f \<longlongrightarrow> l) (at z)" "\<And>l. \<not> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)"
   obtains a where "- {a} \<subseteq> f ` (M - {z})"
@@ -1784,11 +1784,11 @@
   by%unimportant (metis great_Picard [OF M _ holf] non)
     
 
-corollary%important great_Picard_infinite:
+corollary great_Picard_infinite:
   assumes M: "open M" "z \<in> M" and holf: "f holomorphic_on (M - {z})"
     and non: "\<And>l. \<not> (f \<longlongrightarrow> l) (at z)" "\<And>l. \<not> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)"
   obtains a where "\<And>w. w \<noteq> a \<Longrightarrow> infinite {x. x \<in> M - {z} \<and> f x = w}"
-proof%unimportant -
+proof -
   have False if "a \<noteq> b" and ab: "finite {x. x \<in> M - {z} \<and> f x = a}" "finite {x. x \<in> M - {z} \<and> f x = b}" for a b
   proof -
     have finab: "finite {x. x \<in> M - {z} \<and> f x \<in> {a,b}}"
@@ -1830,11 +1830,11 @@
     by meson
 qed
 
-corollary%important Casorati_Weierstrass:
+theorem Casorati_Weierstrass:
   assumes "open M" "z \<in> M" "f holomorphic_on (M - {z})"
       and "\<And>l. \<not> (f \<longlongrightarrow> l) (at z)" "\<And>l. \<not> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)"
   shows "closure(f ` (M - {z})) = UNIV"
-proof%unimportant -
+proof -
   obtain a where a: "- {a} \<subseteq> f ` (M - {z})"
     using great_Picard_alt [OF assms] .
   have "UNIV = closure(- {a})"
--- a/src/HOL/Analysis/Homeomorphism.thy	Wed Jan 16 21:27:33 2019 +0000
+++ b/src/HOL/Analysis/Homeomorphism.thy	Thu Jan 17 15:50:28 2019 +0000
@@ -8,7 +8,7 @@
 imports Homotopy
 begin
 
-lemma%unimportant homeomorphic_spheres':
+lemma homeomorphic_spheres':
   fixes a ::"'a::euclidean_space" and b ::"'b::euclidean_space"
   assumes "0 < \<delta>" and dimeq: "DIM('a) = DIM('b)"
   shows "(sphere a \<delta>) homeomorphic (sphere b \<delta>)"
@@ -28,7 +28,7 @@
     done
 qed
 
-lemma%unimportant homeomorphic_spheres_gen:
+lemma homeomorphic_spheres_gen:
     fixes a :: "'a::euclidean_space" and b :: "'b::euclidean_space"
   assumes "0 < r" "0 < s" "DIM('a::euclidean_space) = DIM('b::euclidean_space)"
   shows "(sphere a r homeomorphic sphere b s)"
@@ -38,7 +38,7 @@
 
 subsection%important \<open>Homeomorphism of all convex compact sets with nonempty interior\<close>
 
-proposition%important ray_to_rel_frontier:
+proposition ray_to_rel_frontier:
   fixes a :: "'a::real_inner"
   assumes "bounded S"
       and a: "a \<in> rel_interior S"
@@ -46,7 +46,7 @@
       and "l \<noteq> 0"
   obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> rel_frontier S"
            "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S"
-proof%unimportant -
+proof -
   have aaff: "a \<in> affine hull S"
     by (meson a hull_subset rel_interior_subset rev_subsetD)
   let ?D = "{d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}"
@@ -139,14 +139,14 @@
     by (rule that [OF \<open>0 < d\<close> infront inint])
 qed
 
-corollary%important ray_to_frontier:
+corollary ray_to_frontier:
   fixes a :: "'a::euclidean_space"
   assumes "bounded S"
       and a: "a \<in> interior S"
       and "l \<noteq> 0"
   obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> frontier S"
            "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> interior S"
-proof%unimportant -
+proof -
   have "interior S = rel_interior S"
     using a rel_interior_nonempty_interior by auto
   then have "a \<in> rel_interior S"
@@ -158,7 +158,7 @@
 qed
 
 
-lemma%unimportant segment_to_rel_frontier_aux:
+lemma segment_to_rel_frontier_aux:
   fixes x :: "'a::euclidean_space"
   assumes "convex S" "bounded S" and x: "x \<in> rel_interior S" and y: "y \<in> S" and xy: "x \<noteq> y"
   obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z"
@@ -198,7 +198,7 @@
   qed
 qed
 
-lemma%unimportant segment_to_rel_frontier:
+lemma segment_to_rel_frontier:
   fixes x :: "'a::euclidean_space"
   assumes S: "convex S" "bounded S" and x: "x \<in> rel_interior S"
       and y: "y \<in> S" and xy: "\<not>(x = y \<and> S = {x})"
@@ -216,11 +216,11 @@
     using segment_to_rel_frontier_aux [OF S x y] that by blast
 qed
 
-proposition%important rel_frontier_not_sing:
+proposition rel_frontier_not_sing:
   fixes a :: "'a::euclidean_space"
   assumes "bounded S"
     shows "rel_frontier S \<noteq> {a}"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
   case True  then show ?thesis  by simp
 next
   case False
@@ -278,7 +278,7 @@
   qed
 qed
 
-proposition%important
+proposition (*FIXME needs name *)
   fixes S :: "'a::euclidean_space set"
   assumes "compact S" and 0: "0 \<in> rel_interior S"
       and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment 0 x \<subseteq> rel_interior S"
@@ -288,7 +288,7 @@
       and starlike_compact_projective2_0:
             "S homeomorphic cball 0 1 \<inter> affine hull S"
             (is "S homeomorphic ?CBALL")
-proof%unimportant -
+proof -
   have starI: "(u *\<^sub>R x) \<in> rel_interior S" if "x \<in> S" "0 \<le> u" "u < 1" for x u
   proof (cases "x=0 \<or> u=0")
     case True with 0 show ?thesis by force
@@ -540,7 +540,7 @@
     done
 qed
 
-corollary%important
+corollary (* FIXME needs name *)
   fixes S :: "'a::euclidean_space set"
   assumes "compact S" and a: "a \<in> rel_interior S"
       and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
@@ -548,7 +548,7 @@
             "S - rel_interior S homeomorphic sphere a 1 \<inter> affine hull S"
       and starlike_compact_projective2:
             "S homeomorphic cball a 1 \<inter> affine hull S"
-proof%unimportant -
+proof -
   have 1: "compact ((+) (-a) ` S)" by (meson assms compact_translation)
   have 2: "0 \<in> rel_interior ((+) (-a) ` S)"
     using a rel_interior_translation [of "- a" S] by (simp cong: image_cong_simp)
@@ -580,12 +580,12 @@
   finally show "S homeomorphic cball a 1 \<inter> affine hull S" .
 qed
 
-corollary%important starlike_compact_projective_special:
+corollary starlike_compact_projective_special:
   assumes "compact S"
     and cb01: "cball (0::'a::euclidean_space) 1 \<subseteq> S"
     and scale: "\<And>x u. \<lbrakk>x \<in> S; 0 \<le> u; u < 1\<rbrakk> \<Longrightarrow> u *\<^sub>R x \<in> S - frontier S"
   shows "S homeomorphic (cball (0::'a::euclidean_space) 1)"
-proof%unimportant -
+proof -
   have "ball 0 1 \<subseteq> interior S"
     using cb01 interior_cball interior_mono by blast
   then have 0: "0 \<in> rel_interior S"
@@ -604,13 +604,13 @@
     using starlike_compact_projective2_0 [OF \<open>compact S\<close> 0 star] by simp
 qed
 
-lemma%important homeomorphic_convex_lemma:
+lemma homeomorphic_convex_lemma:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   assumes "convex S" "compact S" "convex T" "compact T"
       and affeq: "aff_dim S = aff_dim T"
     shows "(S - rel_interior S) homeomorphic (T - rel_interior T) \<and>
            S homeomorphic T"
-proof%unimportant (cases "rel_interior S = {} \<or> rel_interior T = {}")
+proof (cases "rel_interior S = {} \<or> rel_interior T = {}")
   case True
     then show ?thesis
       by (metis Diff_empty affeq \<open>convex S\<close> \<open>convex T\<close> aff_dim_empty homeomorphic_empty rel_interior_eq_empty aff_dim_empty)
@@ -708,7 +708,7 @@
     using 1 2 by blast
 qed
 
-lemma%unimportant homeomorphic_convex_compact_sets:
+lemma homeomorphic_convex_compact_sets:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   assumes "convex S" "compact S" "convex T" "compact T"
       and affeq: "aff_dim S = aff_dim T"
@@ -716,7 +716,7 @@
 using homeomorphic_convex_lemma [OF assms] assms
 by (auto simp: rel_frontier_def)
 
-lemma%unimportant homeomorphic_rel_frontiers_convex_bounded_sets:
+lemma homeomorphic_rel_frontiers_convex_bounded_sets:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   assumes "convex S" "bounded S" "convex T" "bounded T"
       and affeq: "aff_dim S = aff_dim T"
@@ -729,7 +729,7 @@
 text\<open>Including the famous stereoscopic projection of the 3-D sphere to the complex plane\<close>
 
 text\<open>The special case with centre 0 and radius 1\<close>
-lemma%unimportant homeomorphic_punctured_affine_sphere_affine_01:
+lemma homeomorphic_punctured_affine_sphere_affine_01:
   assumes "b \<in> sphere 0 1" "affine T" "0 \<in> T" "b \<in> T" "affine p"
       and affT: "aff_dim T = aff_dim p + 1"
     shows "(sphere 0 1 \<inter> T) - {b} homeomorphic p"
@@ -823,12 +823,12 @@
   finally show ?thesis .
 qed
 
-theorem%important homeomorphic_punctured_affine_sphere_affine:
+theorem homeomorphic_punctured_affine_sphere_affine:
   fixes a :: "'a :: euclidean_space"
   assumes "0 < r" "b \<in> sphere a r" "affine T" "a \<in> T" "b \<in> T" "affine p"
       and aff: "aff_dim T = aff_dim p + 1"
     shows "(sphere a r \<inter> T) - {b} homeomorphic p"
-proof%unimportant -
+proof -
   have "a \<noteq> b" using assms by auto
   then have inj: "inj (\<lambda>x::'a. x /\<^sub>R norm (a - b))"
     by (simp add: inj_on_def)
@@ -847,14 +847,14 @@
   finally show ?thesis .
 qed
 
-corollary%important homeomorphic_punctured_sphere_affine:
+corollary homeomorphic_punctured_sphere_affine:
   fixes a :: "'a :: euclidean_space"
   assumes "0 < r" and b: "b \<in> sphere a r"
       and "affine T" and affS: "aff_dim T + 1 = DIM('a)"
     shows "(sphere a r - {b}) homeomorphic T"
   using%unimportant homeomorphic_punctured_affine_sphere_affine [of r b a UNIV T] assms by%unimportant auto
 
-corollary%important homeomorphic_punctured_sphere_hyperplane:
+corollary homeomorphic_punctured_sphere_hyperplane:
   fixes a :: "'a :: euclidean_space"
   assumes "0 < r" and b: "b \<in> sphere a r"
       and "c \<noteq> 0"
@@ -864,12 +864,12 @@
 apply (auto simp: affine_hyperplane of_nat_diff)
 done
 
-proposition%important homeomorphic_punctured_sphere_affine_gen:
+proposition homeomorphic_punctured_sphere_affine_gen:
   fixes a :: "'a :: euclidean_space"
   assumes "convex S" "bounded S" and a: "a \<in> rel_frontier S"
       and "affine T" and affS: "aff_dim S = aff_dim T + 1"
     shows "rel_frontier S - {a} homeomorphic T"
-proof%unimportant -
+proof -
   obtain U :: "'a set" where "affine U" "convex U" and affdS: "aff_dim U = aff_dim S"
     using choose_affine_subset [OF affine_UNIV aff_dim_geq]
     by (meson aff_dim_affine_hull affine_affine_hull affine_imp_convex)
@@ -912,13 +912,13 @@
   is homeomorphic to a closed subset of a convex set, and
   if the set is locally compact we can take the convex set to be the universe.\<close>
 
-proposition%important homeomorphic_closedin_convex:
+proposition homeomorphic_closedin_convex:
   fixes S :: "'m::euclidean_space set"
   assumes "aff_dim S < DIM('n)"
   obtains U and T :: "'n::euclidean_space set"
      where "convex U" "U \<noteq> {}" "closedin (subtopology euclidean U) T"
            "S homeomorphic T"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
   case True then show ?thesis
     by (rule_tac U=UNIV and T="{}" in that) auto
 next
@@ -1009,11 +1009,11 @@
 text\<open> Locally compact sets are closed in an open set and are homeomorphic
   to an absolutely closed set if we have one more dimension to play with.\<close>
 
-lemma%important locally_compact_open_Int_closure:
+lemma locally_compact_open_Int_closure:
   fixes S :: "'a :: metric_space set"
   assumes "locally compact S"
   obtains T where "open T" "S = T \<inter> closure S"
-proof%unimportant -
+proof -
   have "\<forall>x\<in>S. \<exists>T v u. u = S \<inter> T \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> S \<and> open T \<and> compact v"
     by (metis assms locally_compact openin_open)
   then obtain t v where
@@ -1048,14 +1048,14 @@
 qed
 
 
-lemma%unimportant locally_compact_closedin_open:
+lemma locally_compact_closedin_open:
     fixes S :: "'a :: metric_space set"
     assumes "locally compact S"
     obtains T where "open T" "closedin (subtopology euclidean T) S"
   by (metis locally_compact_open_Int_closure [OF assms] closed_closure closedin_closed_Int)
 
 
-lemma%unimportant locally_compact_homeomorphism_projection_closed:
+lemma locally_compact_homeomorphism_projection_closed:
   assumes "locally compact S"
   obtains T and f :: "'a \<Rightarrow> 'a :: euclidean_space \<times> 'b :: euclidean_space"
     where "closed T" "homeomorphism S T f fst"
@@ -1108,14 +1108,14 @@
       done
 qed
 
-lemma%unimportant locally_compact_closed_Int_open:
+lemma locally_compact_closed_Int_open:
   fixes S :: "'a :: euclidean_space set"
   shows
     "locally compact S \<longleftrightarrow> (\<exists>U u. closed U \<and> open u \<and> S = U \<inter> u)"
 by (metis closed_closure closed_imp_locally_compact inf_commute locally_compact_Int locally_compact_open_Int_closure open_imp_locally_compact)
 
 
-lemma%unimportant lowerdim_embeddings:
+lemma lowerdim_embeddings:
   assumes  "DIM('a) < DIM('b)"
   obtains f :: "'a::euclidean_space*real \<Rightarrow> 'b::euclidean_space" 
       and g :: "'b \<Rightarrow> 'a*real"
@@ -1161,11 +1161,11 @@
   qed
 qed
 
-proposition%important locally_compact_homeomorphic_closed:
+proposition locally_compact_homeomorphic_closed:
   fixes S :: "'a::euclidean_space set"
   assumes "locally compact S" and dimlt: "DIM('a) < DIM('b)"
   obtains T :: "'b::euclidean_space set" where "closed T" "S homeomorphic T"
-proof%unimportant -
+proof -
   obtain U:: "('a*real)set" and h
     where "closed U" and homU: "homeomorphism S U h fst"
     using locally_compact_homeomorphism_projection_closed assms by metis
@@ -1191,13 +1191,13 @@
 qed
 
 
-lemma%important homeomorphic_convex_compact_lemma:
+lemma homeomorphic_convex_compact_lemma:
   fixes S :: "'a::euclidean_space set"
   assumes "convex S"
     and "compact S"
     and "cball 0 1 \<subseteq> S"
   shows "S homeomorphic (cball (0::'a) 1)"
-proof%unimportant (rule starlike_compact_projective_special[OF assms(2-3)])
+proof (rule starlike_compact_projective_special[OF assms(2-3)])
   fix x u
   assume "x \<in> S" and "0 \<le> u" and "u < (1::real)"
   have "open (ball (u *\<^sub>R x) (1 - u))"
@@ -1223,7 +1223,7 @@
     using frontier_def and interior_subset by auto
 qed
 
-proposition%important homeomorphic_convex_compact_cball:
+proposition homeomorphic_convex_compact_cball:
   fixes e :: real
     and S :: "'a::euclidean_space set"
   assumes "convex S"
@@ -1231,7 +1231,7 @@
     and "interior S \<noteq> {}"
     and "e > 0"
   shows "S homeomorphic (cball (b::'a) e)"
-proof%unimportant -
+proof -
   obtain a where "a \<in> interior S"
     using assms(3) by auto
   then obtain d where "d > 0" and d: "cball a d \<subseteq> S"
@@ -1259,7 +1259,7 @@
     done
 qed
 
-corollary%important homeomorphic_convex_compact:
+corollary homeomorphic_convex_compact:
   fixes S :: "'a::euclidean_space set"
     and T :: "'a set"
   assumes "convex S" "compact S" "interior S \<noteq> {}"
@@ -1268,7 +1268,7 @@
   using assms
   by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
 
-subsection%important\<open>Covering spaces and lifting results for them\<close>
+subsection\<open>Covering spaces and lifting results for them\<close>
 
 definition%important covering_space
            :: "'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
@@ -1281,19 +1281,19 @@
                         pairwise disjnt v \<and>
                         (\<forall>u \<in> v. \<exists>q. homeomorphism u T p q)))"
 
-lemma%unimportant covering_space_imp_continuous: "covering_space c p S \<Longrightarrow> continuous_on c p"
+lemma covering_space_imp_continuous: "covering_space c p S \<Longrightarrow> continuous_on c p"
   by (simp add: covering_space_def)
 
-lemma%unimportant covering_space_imp_surjective: "covering_space c p S \<Longrightarrow> p ` c = S"
+lemma covering_space_imp_surjective: "covering_space c p S \<Longrightarrow> p ` c = S"
   by (simp add: covering_space_def)
 
-lemma%unimportant homeomorphism_imp_covering_space: "homeomorphism S T f g \<Longrightarrow> covering_space S f T"
+lemma homeomorphism_imp_covering_space: "homeomorphism S T f g \<Longrightarrow> covering_space S f T"
   apply (simp add: homeomorphism_def covering_space_def, clarify)
   apply (rule_tac x=T in exI, simp)
   apply (rule_tac x="{S}" in exI, auto)
   done
 
-lemma%unimportant covering_space_local_homeomorphism:
+lemma covering_space_local_homeomorphism:
   assumes "covering_space c p S" "x \<in> c"
   obtains T u q where "x \<in> T" "openin (subtopology euclidean c) T"
                       "p x \<in> u" "openin (subtopology euclidean S) u"
@@ -1304,13 +1304,13 @@
   by (metis IntI UnionE vimage_eq) 
 
 
-lemma%important covering_space_local_homeomorphism_alt:
+lemma covering_space_local_homeomorphism_alt:
   assumes p: "covering_space c p S" and "y \<in> S"
   obtains x T U q where "p x = y"
                         "x \<in> T" "openin (subtopology euclidean c) T"
                         "y \<in> U" "openin (subtopology euclidean S) U"
                           "homeomorphism T U p q"
-proof%unimportant -
+proof -
   obtain x where "p x = y" "x \<in> c"
     using assms covering_space_imp_surjective by blast
   show ?thesis
@@ -1318,11 +1318,11 @@
     using that \<open>p x = y\<close> by blast
 qed
 
-proposition%important covering_space_open_map:
+proposition covering_space_open_map:
   fixes S :: "'a :: metric_space set" and T :: "'b :: metric_space set"
   assumes p: "covering_space c p S" and T: "openin (subtopology euclidean c) T"
     shows "openin (subtopology euclidean S) (p ` T)"
-proof%unimportant -
+proof -
   have pce: "p ` c = S"
    and covs:
        "\<And>x. x \<in> S \<Longrightarrow>
@@ -1368,7 +1368,7 @@
   with openin_subopen show ?thesis by blast
 qed
 
-lemma%important covering_space_lift_unique_gen:
+lemma covering_space_lift_unique_gen:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
   assumes cov: "covering_space c p S"
@@ -1380,7 +1380,7 @@
       and fg2: "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)"
       and u_compt: "U \<in> components T" and "a \<in> U" "x \<in> U"
     shows "g1 x = g2 x"
-proof%unimportant -
+proof -
   have "U \<subseteq> T" by (rule in_components_subset [OF u_compt])
   define G12 where "G12 \<equiv> {x \<in> U. g1 x - g2 x = 0}"
   have "connected U" by (rule in_components_connected [OF u_compt])
@@ -1427,7 +1427,7 @@
     using \<open>x \<in> U\<close> by force
 qed
 
-proposition%important covering_space_lift_unique:
+proposition covering_space_lift_unique:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
   assumes "covering_space c p S"
@@ -1437,10 +1437,10 @@
           "continuous_on T g2"  "g2 ` T \<subseteq> c"  "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)"
           "connected T"  "a \<in> T"   "x \<in> T"
    shows "g1 x = g2 x"
-  using%unimportant covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv
-  by%unimportant blast
+  using covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv
+  by blast
 
-lemma%unimportant covering_space_locally:
+lemma covering_space_locally:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes loc: "locally \<phi> C" and cov: "covering_space C p S"
       and pim: "\<And>T. \<lbrakk>T \<subseteq> C; \<phi> T\<rbrakk> \<Longrightarrow> \<psi>(p ` T)"
@@ -1456,14 +1456,14 @@
 qed
 
 
-proposition%important covering_space_locally_eq:
+proposition covering_space_locally_eq:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes cov: "covering_space C p S"
       and pim: "\<And>T. \<lbrakk>T \<subseteq> C; \<phi> T\<rbrakk> \<Longrightarrow> \<psi>(p ` T)"
       and qim: "\<And>q U. \<lbrakk>U \<subseteq> S; continuous_on U q; \<psi> U\<rbrakk> \<Longrightarrow> \<phi>(q ` U)"
     shows "locally \<psi> S \<longleftrightarrow> locally \<phi> C"
          (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume L: ?lhs
   show ?rhs
   proof (rule locallyI)
@@ -1518,7 +1518,7 @@
     using cov covering_space_locally pim by blast
 qed
 
-lemma%unimportant covering_space_locally_compact_eq:
+lemma covering_space_locally_compact_eq:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "covering_space C p S"
   shows "locally compact S \<longleftrightarrow> locally compact C"
@@ -1526,7 +1526,7 @@
    apply (meson assms compact_continuous_image continuous_on_subset covering_space_imp_continuous)
   using compact_continuous_image by blast
 
-lemma%unimportant covering_space_locally_connected_eq:
+lemma covering_space_locally_connected_eq:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "covering_space C p S"
     shows "locally connected S \<longleftrightarrow> locally connected C"
@@ -1534,7 +1534,7 @@
    apply (meson connected_continuous_image assms continuous_on_subset covering_space_imp_continuous)
   using connected_continuous_image by blast
 
-lemma%unimportant covering_space_locally_path_connected_eq:
+lemma covering_space_locally_path_connected_eq:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "covering_space C p S"
     shows "locally path_connected S \<longleftrightarrow> locally path_connected C"
@@ -1543,26 +1543,26 @@
   using path_connected_continuous_image by blast
 
 
-lemma%unimportant covering_space_locally_compact:
+lemma covering_space_locally_compact:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "locally compact C" "covering_space C p S"
   shows "locally compact S"
   using assms covering_space_locally_compact_eq by blast
 
 
-lemma%unimportant covering_space_locally_connected:
+lemma covering_space_locally_connected:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "locally connected C" "covering_space C p S"
   shows "locally connected S"
   using assms covering_space_locally_connected_eq by blast
 
-lemma%unimportant covering_space_locally_path_connected:
+lemma covering_space_locally_path_connected:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "locally path_connected C" "covering_space C p S"
   shows "locally path_connected S"
   using assms covering_space_locally_path_connected_eq by blast
 
-proposition%important covering_space_lift_homotopy:
+proposition covering_space_lift_homotopy:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
     and h :: "real \<times> 'c::real_normed_vector \<Rightarrow> 'b"
   assumes cov: "covering_space C p S"
@@ -1574,7 +1574,7 @@
                     "k ` ({0..1} \<times> U) \<subseteq> C"
                     "\<And>y. y \<in> U \<Longrightarrow> k(0, y) = f y"
                     "\<And>z. z \<in> {0..1} \<times> U \<Longrightarrow> h z = p(k z)"
-proof%unimportant -
+proof -
   have "\<exists>V k. openin (subtopology euclidean U) V \<and> y \<in> V \<and>
               continuous_on ({0..1} \<times> V) k \<and> k ` ({0..1} \<times> V) \<subseteq> C \<and>
               (\<forall>z \<in> V. k(0, z) = f z) \<and> (\<forall>z \<in> {0..1} \<times> V. h z = p(k z))"
@@ -1912,7 +1912,7 @@
   qed (auto simp: contk)
 qed
 
-corollary%important covering_space_lift_homotopy_alt:
+corollary covering_space_lift_homotopy_alt:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
     and h :: "'c::real_normed_vector \<times> real \<Rightarrow> 'b"
   assumes cov: "covering_space C p S"
@@ -1924,7 +1924,7 @@
                   "k ` (U \<times> {0..1}) \<subseteq> C"
                   "\<And>y. y \<in> U \<Longrightarrow> k(y, 0) = f y"
                   "\<And>z. z \<in> U \<times> {0..1} \<Longrightarrow> h z = p(k z)"
-proof%unimportant -
+proof -
   have "continuous_on ({0..1} \<times> U) (h \<circ> (\<lambda>z. (snd z, fst z)))"
     by (intro continuous_intros continuous_on_subset [OF conth]) auto
   then obtain k where contk: "continuous_on ({0..1} \<times> U) k"
@@ -1940,7 +1940,7 @@
     done
 qed
 
-corollary%important covering_space_lift_homotopic_function:
+corollary covering_space_lift_homotopic_function:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" and g:: "'c::real_normed_vector \<Rightarrow> 'a"
   assumes cov: "covering_space C p S"
       and contg: "continuous_on U g"
@@ -1948,7 +1948,7 @@
       and pgeq: "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
       and hom: "homotopic_with (\<lambda>x. True) U S f f'"
     obtains g' where "continuous_on U g'" "image g' U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g' y) = f' y"
-proof%unimportant -
+proof -
   obtain h where conth: "continuous_on ({0..1::real} \<times> U) h"
              and him: "h ` ({0..1} \<times> U) \<subseteq> S"
              and h0:  "\<And>x. h(0, x) = f x"
@@ -1972,12 +1972,12 @@
   qed
 qed
 
-corollary%important covering_space_lift_inessential_function:
+corollary covering_space_lift_inessential_function:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" and U :: "'c::real_normed_vector set"
   assumes cov: "covering_space C p S"
       and hom: "homotopic_with (\<lambda>x. True) U S f (\<lambda>x. a)"
   obtains g where "continuous_on U g" "g ` U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant (cases "U = {}")
+proof (cases "U = {}")
   case True
   then show ?thesis
     using that continuous_on_empty by blast
@@ -1997,14 +1997,14 @@
 
 subsection%important\<open> Lifting of general functions to covering space\<close>
 
-proposition%important covering_space_lift_path_strong:
+proposition covering_space_lift_path_strong:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
     and f :: "'c::real_normed_vector \<Rightarrow> 'b"
   assumes cov: "covering_space C p S" and "a \<in> C"
       and "path g" and pag: "path_image g \<subseteq> S" and pas: "pathstart g = p a"
     obtains h where "path h" "path_image h \<subseteq> C" "pathstart h = a"
                 and "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h t) = g t"
-proof%unimportant -
+proof -
   obtain k:: "real \<times> 'c \<Rightarrow> 'a"
     where contk: "continuous_on ({0..1} \<times> {undefined}) k"
       and kim: "k ` ({0..1} \<times> {undefined}) \<subseteq> C"
@@ -2033,11 +2033,11 @@
   qed
 qed
 
-corollary%important covering_space_lift_path:
+corollary covering_space_lift_path:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes cov: "covering_space C p S" and "path g" and pig: "path_image g \<subseteq> S"
   obtains h where "path h" "path_image h \<subseteq> C" "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h t) = g t"
-proof%unimportant -
+proof -
   obtain a where "a \<in> C" "pathstart g = p a"
     by (metis pig cov covering_space_imp_surjective imageE pathstart_in_path_image subsetCE)
   show ?thesis
@@ -2046,7 +2046,7 @@
 qed
 
   
-proposition%important covering_space_lift_homotopic_paths:
+proposition covering_space_lift_homotopic_paths:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes cov: "covering_space C p S"
       and "path g1" and pig1: "path_image g1 \<subseteq> S"
@@ -2056,7 +2056,7 @@
       and "path h2" and pih2: "path_image h2 \<subseteq> C" and ph2: "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h2 t) = g2 t"
       and h1h2: "pathstart h1 = pathstart h2"
     shows "homotopic_paths C h1 h2"
-proof%unimportant -
+proof -
   obtain h :: "real \<times> real \<Rightarrow> 'b"
      where conth: "continuous_on ({0..1} \<times> {0..1}) h"
        and him: "h ` ({0..1} \<times> {0..1}) \<subseteq> S"
@@ -2117,7 +2117,7 @@
 qed
 
 
-corollary%important covering_space_monodromy:
+corollary covering_space_monodromy:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes cov: "covering_space C p S"
       and "path g1" and pig1: "path_image g1 \<subseteq> S"
@@ -2131,7 +2131,7 @@
   by%unimportant blast
 
 
-corollary%important covering_space_lift_homotopic_path:
+corollary covering_space_lift_homotopic_path:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes cov: "covering_space C p S"
       and hom: "homotopic_paths S f f'"
@@ -2140,7 +2140,7 @@
       and pgeq: "\<And>t. t \<in> {0..1} \<Longrightarrow> p(g t) = f t"
   obtains g' where "path g'" "path_image g' \<subseteq> C"
                    "pathstart g' = a" "pathfinish g' = b" "\<And>t. t \<in> {0..1} \<Longrightarrow> p(g' t) = f' t"
-proof%unimportant (rule covering_space_lift_path_strong [OF cov, of a f'])
+proof (rule covering_space_lift_path_strong [OF cov, of a f'])
   show "a \<in> C"
     using a pig by auto
   show "path f'" "path_image f' \<subseteq> S"
@@ -2150,7 +2150,7 @@
 qed (metis (mono_tags, lifting) assms cov covering_space_monodromy hom homotopic_paths_imp_path homotopic_paths_imp_subset pgeq pig)
 
 
-proposition%important covering_space_lift_general:
+proposition covering_space_lift_general:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
     and f :: "'c::real_normed_vector \<Rightarrow> 'b"
   assumes cov: "covering_space C p S" and "a \<in> C" "z \<in> U"
@@ -2162,7 +2162,7 @@
                              pathstart q = a \<and> pathfinish q = a \<and>
                              homotopic_paths S (f \<circ> r) (p \<circ> q)"
   obtains g where "continuous_on U g" "g ` U \<subseteq> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant -
+proof -
   have *: "\<exists>g h. path g \<and> path_image g \<subseteq> U \<and>
                  pathstart g = z \<and> pathfinish g = y \<and>
                  path h \<and> path_image h \<subseteq> C \<and> pathstart h = a \<and>
@@ -2405,7 +2405,7 @@
 qed
 
 
-corollary%important covering_space_lift_stronger:
+corollary covering_space_lift_stronger:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
     and f :: "'c::real_normed_vector \<Rightarrow> 'b"
   assumes cov: "covering_space C p S" "a \<in> C" "z \<in> U"
@@ -2415,7 +2415,7 @@
       and hom: "\<And>r. \<lbrakk>path r; path_image r \<subseteq> U; pathstart r = z; pathfinish r = z\<rbrakk>
                      \<Longrightarrow> \<exists>b. homotopic_paths S (f \<circ> r) (linepath b b)"
   obtains g where "continuous_on U g" "g ` U \<subseteq> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant (rule covering_space_lift_general [OF cov U contf fim feq])
+proof (rule covering_space_lift_general [OF cov U contf fim feq])
   fix r
   assume "path r" "path_image r \<subseteq> U" "pathstart r = z" "pathfinish r = z"
   then obtain b where b: "homotopic_paths S (f \<circ> r) (linepath b b)"
@@ -2432,7 +2432,7 @@
     by (force simp: \<open>a \<in> C\<close>)
 qed auto
 
-corollary%important covering_space_lift_strong:
+corollary covering_space_lift_strong:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
     and f :: "'c::real_normed_vector \<Rightarrow> 'b"
   assumes cov: "covering_space C p S" "a \<in> C" "z \<in> U"
@@ -2440,7 +2440,7 @@
       and contf: "continuous_on U f" and fim: "f ` U \<subseteq> S"
       and feq: "f z = p a"
   obtains g where "continuous_on U g" "g ` U \<subseteq> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant (rule covering_space_lift_stronger [OF cov _ lpcU contf fim feq])
+proof (rule covering_space_lift_stronger [OF cov _ lpcU contf fim feq])
   show "path_connected U"
     using scU simply_connected_eq_contractible_loop_some by blast
   fix r
@@ -2453,14 +2453,14 @@
     by blast
 qed blast
 
-corollary%important covering_space_lift:
+corollary covering_space_lift:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
     and f :: "'c::real_normed_vector \<Rightarrow> 'b"
   assumes cov: "covering_space C p S"
       and U: "simply_connected U"  "locally path_connected U"
       and contf: "continuous_on U f" and fim: "f ` U \<subseteq> S"
     obtains g where "continuous_on U g" "g ` U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant (cases "U = {}")
+proof (cases "U = {}")
   case True
   with that show ?thesis by auto
 next
--- a/src/HOL/Analysis/Improper_Integral.thy	Wed Jan 16 21:27:33 2019 +0000
+++ b/src/HOL/Analysis/Improper_Integral.thy	Thu Jan 17 15:50:28 2019 +0000
@@ -28,11 +28,11 @@
   unfolding equiintegrable_on_def Ball_def
   by (erule conj_forward imp_forward all_forward ex_forward | blast)+
 
-lemma%important equiintegrable_on_Un:
+lemma equiintegrable_on_Un:
   assumes "F equiintegrable_on I" "G equiintegrable_on I"
   shows "(F \<union> G) equiintegrable_on I"
   unfolding equiintegrable_on_def
-proof%unimportant (intro conjI impI allI)
+proof (intro conjI impI allI)
   show "\<forall>f\<in>F \<union> G. f integrable_on I"
     using assms unfolding equiintegrable_on_def by blast
   show "\<exists>\<gamma>. gauge \<gamma> \<and>
@@ -76,12 +76,12 @@
 
 text\<open> Main limit theorem for an equiintegrable sequence.\<close>
 
-theorem%important equiintegrable_limit:
+theorem equiintegrable_limit:
   fixes g :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
   assumes feq: "range f equiintegrable_on cbox a b"
       and to_g: "\<And>x. x \<in> cbox a b \<Longrightarrow> (\<lambda>n. f n x) \<longlonglongrightarrow> g x"
     shows "g integrable_on cbox a b \<and> (\<lambda>n. integral (cbox a b) (f n)) \<longlonglongrightarrow> integral (cbox a b) g"
-proof%unimportant -
+proof -
   have "Cauchy (\<lambda>n. integral(cbox a b) (f n))"
   proof (clarsimp simp add: Cauchy_def)
     fix e::real
@@ -151,10 +151,10 @@
 qed
 
 
-lemma%important equiintegrable_reflect:
+lemma equiintegrable_reflect:
   assumes "F equiintegrable_on cbox a b"
   shows "(\<lambda>f. f \<circ> uminus) ` F equiintegrable_on cbox (-b) (-a)"
-proof%unimportant -
+proof -
   have "\<exists>\<gamma>. gauge \<gamma> \<and>
             (\<forall>f \<D>. f \<in> (\<lambda>f. f \<circ> uminus) ` F \<and> \<D> tagged_division_of cbox (- b) (- a) \<and> \<gamma> fine \<D> \<longrightarrow>
                    norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral (cbox (- b) (- a)) f) < e)"
@@ -246,13 +246,13 @@
 qed
 
 
-lemma%important content_division_lemma1:
+lemma content_division_lemma1:
   assumes div: "\<D> division_of S" and S: "S \<subseteq> cbox a b" and i: "i \<in> Basis"
       and mt: "\<And>K. K \<in> \<D> \<Longrightarrow> content K \<noteq> 0"
       and disj: "(\<forall>K \<in> \<D>. K \<inter> {x. x \<bullet> i = a \<bullet> i} \<noteq> {}) \<or> (\<forall>K \<in> \<D>. K \<inter> {x. x \<bullet> i = b \<bullet> i} \<noteq> {})"
    shows "(b \<bullet> i - a \<bullet> i) * (\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))
           \<le> content(cbox a b)"   (is "?lhs \<le> ?rhs")
-proof%unimportant -
+proof -
   have "finite \<D>"
     using div by blast
   define extend where
@@ -409,13 +409,13 @@
 qed
 
 
-proposition%important sum_content_area_over_thin_division:
+proposition sum_content_area_over_thin_division:
   assumes div: "\<D> division_of S" and S: "S \<subseteq> cbox a b" and i: "i \<in> Basis"
     and "a \<bullet> i \<le> c" "c \<le> b \<bullet> i"
     and nonmt: "\<And>K. K \<in> \<D> \<Longrightarrow> K \<inter> {x. x \<bullet> i = c} \<noteq> {}"
   shows "(b \<bullet> i - a \<bullet> i) * (\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))
           \<le> 2 * content(cbox a b)"
-proof%unimportant (cases "content(cbox a b) = 0")
+proof (cases "content(cbox a b) = 0")
   case True
   have "(\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) = 0"
     using S div by (force intro!: sum.neutral content_0_subset [OF True])
@@ -609,7 +609,7 @@
 
 
 
-proposition%important bounded_equiintegral_over_thin_tagged_partial_division:
+proposition bounded_equiintegral_over_thin_tagged_partial_division:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes F: "F equiintegrable_on cbox a b" and f: "f \<in> F" and "0 < \<epsilon>"
       and norm_f: "\<And>h x. \<lbrakk>h \<in> F; x \<in> cbox a b\<rbrakk> \<Longrightarrow> norm(h x) \<le> norm(f x)"
@@ -617,7 +617,7 @@
              "\<And>c i S h. \<lbrakk>c \<in> cbox a b; i \<in> Basis; S tagged_partial_division_of cbox a b;
                          \<gamma> fine S; h \<in> F; \<And>x K. (x,K) \<in> S \<Longrightarrow> (K \<inter> {x. x \<bullet> i = c \<bullet> i} \<noteq> {})\<rbrakk>
                         \<Longrightarrow> (\<Sum>(x,K) \<in> S. norm (integral K h)) < \<epsilon>"
-proof%unimportant (cases "content(cbox a b) = 0")
+proof (cases "content(cbox a b) = 0")
   case True
   show ?thesis
   proof
@@ -813,13 +813,13 @@
 
 
 
-proposition%important equiintegrable_halfspace_restrictions_le:
+proposition equiintegrable_halfspace_restrictions_le:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes F: "F equiintegrable_on cbox a b" and f: "f \<in> F"
     and norm_f: "\<And>h x. \<lbrakk>h \<in> F; x \<in> cbox a b\<rbrakk> \<Longrightarrow> norm(h x) \<le> norm(f x)"
   shows "(\<Union>i \<in> Basis. \<Union>c. \<Union>h \<in> F. {(\<lambda>x. if x \<bullet> i \<le> c then h x else 0)})
          equiintegrable_on cbox a b"
-proof%unimportant (cases "content(cbox a b) = 0")
+proof (cases "content(cbox a b) = 0")
   case True
   then show ?thesis by simp
 next
@@ -1172,13 +1172,13 @@
 
 
 
-corollary%important equiintegrable_halfspace_restrictions_ge:
+corollary equiintegrable_halfspace_restrictions_ge:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes F: "F equiintegrable_on cbox a b" and f: "f \<in> F"
     and norm_f: "\<And>h x. \<lbrakk>h \<in> F; x \<in> cbox a b\<rbrakk> \<Longrightarrow> norm(h x) \<le> norm(f x)"
   shows "(\<Union>i \<in> Basis. \<Union>c. \<Union>h \<in> F. {(\<lambda>x. if x \<bullet> i \<ge> c then h x else 0)})
          equiintegrable_on cbox a b"
-proof%unimportant -
+proof -
   have *: "(\<Union>i\<in>Basis. \<Union>c. \<Union>h\<in>(\<lambda>f. f \<circ> uminus) ` F. {\<lambda>x. if x \<bullet> i \<le> c then h x else 0})
            equiintegrable_on  cbox (- b) (- a)"
   proof (rule equiintegrable_halfspace_restrictions_le)
@@ -1203,11 +1203,11 @@
 qed
 
 
-proposition%important equiintegrable_closed_interval_restrictions:
+proposition equiintegrable_closed_interval_restrictions:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes f: "f integrable_on cbox a b"
   shows "(\<Union>c d. {(\<lambda>x. if x \<in> cbox c d then f x else 0)}) equiintegrable_on cbox a b"
-proof%unimportant -
+proof -
   let ?g = "\<lambda>B c d x. if \<forall>i\<in>B. c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i then f x else 0"
   have *: "insert f (\<Union>c d. {?g B c d}) equiintegrable_on cbox a b" if "B \<subseteq> Basis" for B
   proof -
@@ -1266,14 +1266,14 @@
 
 subsection%important\<open>Continuity of the indefinite integral\<close>
 
-proposition%important indefinite_integral_continuous:
+proposition indefinite_integral_continuous:
   fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
   assumes int_f: "f integrable_on cbox a b"
       and c: "c \<in> cbox a b" and d: "d \<in> cbox a b" "0 < \<epsilon>"
   obtains \<delta> where "0 < \<delta>"
               "\<And>c' d'. \<lbrakk>c' \<in> cbox a b; d' \<in> cbox a b; norm(c' - c) \<le> \<delta>; norm(d' - d) \<le> \<delta>\<rbrakk>
                         \<Longrightarrow> norm(integral(cbox c' d') f - integral(cbox c d) f) < \<epsilon>"
-proof%unimportant -
+proof -
   { assume "\<exists>c' d'. c' \<in> cbox a b \<and> d' \<in> cbox a b \<and> norm(c' - c) \<le> \<delta> \<and> norm(d' - d) \<le> \<delta> \<and>
                     norm(integral(cbox c' d') f - integral(cbox c d) f) \<ge> \<epsilon>"
                     (is "\<exists>c' d'. ?\<Phi> c' d' \<delta>") if "0 < \<delta>" for \<delta>
@@ -1358,11 +1358,11 @@
     by (meson not_le that)
 qed
 
-corollary%important indefinite_integral_uniformly_continuous:
+corollary indefinite_integral_uniformly_continuous:
   fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
   assumes "f integrable_on cbox a b"
   shows "uniformly_continuous_on (cbox (Pair a a) (Pair b b)) (\<lambda>y. integral (cbox (fst y) (snd y)) f)"
-proof%unimportant -
+proof -
   show ?thesis
   proof (rule compact_uniformly_continuous, clarsimp simp add: continuous_on_iff)
     fix c d and \<epsilon>::real
@@ -1383,11 +1383,11 @@
 qed
 
 
-corollary%important bounded_integrals_over_subintervals:
+corollary bounded_integrals_over_subintervals:
   fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
   assumes "f integrable_on cbox a b"
   shows "bounded {integral (cbox c d) f |c d. cbox c d \<subseteq> cbox a b}"
-proof%unimportant -
+proof -
   have "bounded ((\<lambda>y. integral (cbox (fst y) (snd y)) f) ` cbox (a, a) (b, b))"
        (is "bounded ?I")
     by (blast intro: bounded_cbox bounded_uniformly_continuous_image indefinite_integral_uniformly_continuous [OF assms])
@@ -1414,7 +1414,7 @@
 We only need to assume that the integrals are bounded, and we get absolute integrability,
 but we also need a (rather weak) bound assumption on the function.\<close>
 
-theorem%important absolutely_integrable_improper:
+theorem absolutely_integrable_improper:
   fixes f :: "'M::euclidean_space \<Rightarrow> 'N::euclidean_space"
   assumes int_f: "\<And>c d. cbox c d \<subseteq> box a b \<Longrightarrow> f integrable_on cbox c d"
       and bo: "bounded {integral (cbox c d) f |c d. cbox c d \<subseteq> box a b}"
@@ -1422,7 +1422,7 @@
           \<Longrightarrow> \<exists>g. g absolutely_integrable_on cbox a b \<and>
                   ((\<forall>x \<in> cbox a b. f x \<bullet> i \<le> g x) \<or> (\<forall>x \<in> cbox a b. f x \<bullet> i \<ge> g x))"
       shows "f absolutely_integrable_on cbox a b"
-proof%unimportant (cases "content(cbox a b) = 0")
+proof (cases "content(cbox a b) = 0")
   case True
   then show ?thesis
     by auto
--- a/src/HOL/Analysis/Interval_Integral.thy	Wed Jan 16 21:27:33 2019 +0000
+++ b/src/HOL/Analysis/Interval_Integral.thy	Thu Jan 17 15:50:28 2019 +0000
@@ -4,15 +4,15 @@
 Lebesgue integral over an interval (with endpoints possibly +-\<infinity>)
 *)
 
-theory Interval_Integral
+theory Interval_Integral (*FIX ME rename? Lebesgue  *)
   imports Equivalence_Lebesgue_Henstock_Integration
 begin
 
-lemma%important continuous_on_vector_derivative:
+lemma continuous_on_vector_derivative:
   "(\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f"
-  by%unimportant (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)
+  by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)
 
-definition%important "einterval a b = {x. a < ereal x \<and> ereal x < b}"
+definition "einterval a b = {x. a < ereal x \<and> ereal x < b}"
 
 lemma einterval_eq[simp]:
   shows einterval_eq_Icc: "einterval (ereal a) (ereal b) = {a <..< b}"
@@ -37,16 +37,16 @@
 lemma borel_einterval[measurable]: "einterval a b \<in> sets borel"
   unfolding einterval_def by measurable
 
-subsection\<open>Approximating a (possibly infinite) interval\<close>
+subsection%important \<open>Approximating a (possibly infinite) interval\<close>
 
 lemma filterlim_sup1: "(LIM x F. f x :> G1) \<Longrightarrow> (LIM x F. f x :> (sup G1 G2))"
  unfolding filterlim_def by (auto intro: le_supI1)
 
-lemma%important ereal_incseq_approx:
+lemma ereal_incseq_approx:
   fixes a b :: ereal
   assumes "a < b"
   obtains X :: "nat \<Rightarrow> real" where "incseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> b"
-proof%unimportant (cases b)
+proof (cases b)
   case PInf
   with \<open>a < b\<close> have "a = -\<infinity> \<or> (\<exists>r. a = ereal r)"
     by (cases a) auto
@@ -78,12 +78,12 @@
        (auto simp: real incseq_def intro!: divide_left_mono)
 qed (insert \<open>a < b\<close>, auto)
 
-lemma%important ereal_decseq_approx:
+lemma ereal_decseq_approx:
   fixes a b :: ereal
   assumes "a < b"
   obtains X :: "nat \<Rightarrow> real" where
     "decseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> a"
-proof%unimportant -
+proof -
   have "-b < -a" using \<open>a < b\<close> by simp
   from ereal_incseq_approx[OF this] guess X .
   then show thesis
@@ -93,14 +93,14 @@
     done
 qed
 
-lemma%important einterval_Icc_approximation:
+proposition einterval_Icc_approximation:
   fixes a b :: ereal
   assumes "a < b"
   obtains u l :: "nat \<Rightarrow> real" where
     "einterval a b = (\<Union>i. {l i .. u i})"
     "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
     "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
-proof%unimportant -
+proof -
   from dense[OF \<open>a < b\<close>] obtain c where "a < c" "c < b" by safe
   from ereal_incseq_approx[OF \<open>c < b\<close>] guess u . note u = this
   from ereal_decseq_approx[OF \<open>a < c\<close>] guess l . note l = this
@@ -202,17 +202,17 @@
     interval_lebesgue_integrable M a b (\<lambda>x. c * f x)"
   by (simp add: interval_lebesgue_integrable_def)
 
-lemma%important interval_lebesgue_integrable_mult_left [intro, simp]:
+lemma interval_lebesgue_integrable_mult_left [intro, simp]:
   fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
   shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
     interval_lebesgue_integrable M a b (\<lambda>x. f x * c)"
-  by%unimportant (simp add: interval_lebesgue_integrable_def)
+  by (simp add: interval_lebesgue_integrable_def)
 
-lemma%important interval_lebesgue_integrable_divide [intro, simp]:
+lemma interval_lebesgue_integrable_divide [intro, simp]:
   fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}"
   shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
     interval_lebesgue_integrable M a b (\<lambda>x. f x / c)"
-  by%unimportant (simp add: interval_lebesgue_integrable_def)
+  by (simp add: interval_lebesgue_integrable_def)
 
 lemma interval_lebesgue_integral_mult_right [simp]:
   fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
@@ -220,11 +220,11 @@
     c * interval_lebesgue_integral M a b f"
   by (simp add: interval_lebesgue_integral_def)
 
-lemma%important interval_lebesgue_integral_mult_left [simp]:
+lemma interval_lebesgue_integral_mult_left [simp]:
   fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
   shows "interval_lebesgue_integral M a b (\<lambda>x. f x * c) =
     interval_lebesgue_integral M a b f * c"
-  by%unimportant (simp add: interval_lebesgue_integral_def)
+  by (simp add: interval_lebesgue_integral_def)
 
 lemma interval_lebesgue_integral_divide [simp]:
   fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}"
@@ -242,11 +242,11 @@
   unfolding interval_lebesgue_integral_def
   by (auto simp: interval_lebesgue_integral_def set_integral_complex_of_real)
 
-lemma%important interval_lebesgue_integral_le_eq:
+lemma interval_lebesgue_integral_le_eq:
   fixes a b f
   assumes "a \<le> b"
   shows "interval_lebesgue_integral M a b f = (LINT x : einterval a b | M. f x)"
-using%unimportant assms by (auto simp: interval_lebesgue_integral_def)
+  using assms by (auto simp: interval_lebesgue_integral_def)
 
 lemma interval_lebesgue_integral_gt_eq:
   fixes a b f
@@ -271,9 +271,9 @@
     interval_lebesgue_integrable lborel b a f"
   by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integrable_def einterval_same)
 
-lemma%important interval_integral_reflect:
+lemma interval_integral_reflect:
   "(LBINT x=a..b. f x) = (LBINT x=-b..-a. f (-x))"
-proof%unimportant (induct a b rule: linorder_wlog)
+proof (induct a b rule: linorder_wlog)
   case (sym a b) then show ?case
     by (auto simp: interval_lebesgue_integral_def interval_integrable_endpoints_reverse
              split: if_split_asm)
@@ -299,7 +299,7 @@
 lemma interval_integral_to_infinity_eq: "(LINT x=ereal a..\<infinity> | M. f x) = (LINT x : {a<..} | M. f x)"
   unfolding interval_lebesgue_integral_def by auto
 
-lemma%important interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \<infinity> f) =
+proposition interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \<infinity> f) =
   (set_integrable M {a<..} f)"
   unfolding%unimportant interval_lebesgue_integrable_def by auto
 
@@ -317,12 +317,12 @@
   unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq
   by (auto simp: less_imp_le field_simps measure_def set_integrable_def set_lebesgue_integral_def)
 
-lemma%important interval_integral_cong_AE:
+lemma interval_integral_cong_AE:
   assumes [measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel"
   assumes "AE x \<in> einterval (min a b) (max a b) in lborel. f x = g x"
   shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
   using assms
-proof%unimportant (induct a b rule: linorder_wlog)
+proof (induct a b rule: linorder_wlog)
   case (sym a b) then show ?case
     by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b])
 next
@@ -331,11 +331,11 @@
              intro!: set_lebesgue_integral_cong_AE)
 qed
 
-lemma%important interval_integral_cong:
+lemma interval_integral_cong:
   assumes "\<And>x. x \<in> einterval (min a b) (max a b) \<Longrightarrow> f x = g x"
   shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
   using assms
-proof%unimportant (induct a b rule: linorder_wlog)
+proof (induct a b rule: linorder_wlog)
   case (sym a b) then show ?case
     by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b])
 next
@@ -407,11 +407,11 @@
   apply (auto simp: eq anti_eq einterval_iff split: split_indicator)
   done
 
-lemma%important interval_integral_sum:
+lemma interval_integral_sum:
   fixes a b c :: ereal
   assumes integrable: "interval_lebesgue_integrable lborel (min a (min b c)) (max a (max b c)) f"
   shows "(LBINT x=a..b. f x) + (LBINT x=b..c. f x) = (LBINT x=a..c. f x)"
-proof%unimportant -
+proof -
   let ?I = "\<lambda>a b. LBINT x=a..b. f x"
   { fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a \<le> b" "b \<le> c"
     then have ord: "a \<le> b" "b \<le> c" "a \<le> c" and f': "set_integrable lborel (einterval a c) f"
@@ -446,11 +446,11 @@
        (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3)
 qed
 
-lemma%important interval_integrable_isCont:
+lemma interval_integrable_isCont:
   fixes a b and f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
   shows "(\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> isCont f x) \<Longrightarrow>
     interval_lebesgue_integrable lborel a b f"
-proof%unimportant (induct a b rule: linorder_wlog)
+proof (induct a b rule: linorder_wlog)
   case (le a b) then show ?case
     unfolding interval_lebesgue_integrable_def set_integrable_def
     by (auto simp: interval_lebesgue_integrable_def
@@ -478,7 +478,7 @@
 
 subsection%important\<open>General limit approximation arguments\<close>
 
-lemma%important interval_integral_Icc_approx_nonneg:
+proposition interval_integral_Icc_approx_nonneg:
   fixes a b :: ereal
   assumes "a < b"
   fixes u l :: "nat \<Rightarrow> real"
@@ -493,7 +493,7 @@
   shows
     "set_integrable lborel (einterval a b) f"
     "(LBINT x=a..b. f x) = C"
-proof%unimportant -
+proof -
   have 1 [unfolded set_integrable_def]: "\<And>i. set_integrable lborel {l i..u i} f" by (rule f_integrable)
   have 2: "AE x in lborel. mono (\<lambda>n. indicator {l n..u n} x *\<^sub>R f x)"
   proof -
@@ -534,7 +534,7 @@
     by (rule integrable_monotone_convergence[OF 1 2 3 4 5])
 qed
 
-lemma%important interval_integral_Icc_approx_integrable:
+proposition interval_integral_Icc_approx_integrable:
   fixes u l :: "nat \<Rightarrow> real" and a b :: ereal
   fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
   assumes "a < b"
@@ -543,7 +543,7 @@
     "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
   assumes f_integrable: "set_integrable lborel (einterval a b) f"
   shows "(\<lambda>i. LBINT x=l i.. u i. f x) \<longlonglongrightarrow> (LBINT x=a..b. f x)"
-proof%unimportant -
+proof -
   have "(\<lambda>i. LBINT x:{l i.. u i}. f x) \<longlonglongrightarrow> (LBINT x:einterval a b. f x)"
     unfolding set_lebesgue_integral_def
   proof (rule integral_dominated_convergence)
@@ -580,13 +580,13 @@
   TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.)
 *)
 
-lemma%important interval_integral_FTC_finite:
+lemma interval_integral_FTC_finite:
   fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: real
   assumes f: "continuous_on {min a b..max a b} f"
   assumes F: "\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> (F has_vector_derivative (f x)) (at x within
     {min a b..max a b})"
   shows "(LBINT x=a..b. f x) = F b - F a"
-proof%unimportant (cases "a \<le> b")
+proof (cases "a \<le> b")
   case True
   have "(LBINT x=a..b. f x) = (LBINT x. indicat_real {a..b} x *\<^sub>R f x)"
     by (simp add: True interval_integral_Icc set_lebesgue_integral_def)
@@ -617,7 +617,7 @@
 qed
 
 
-lemma%important interval_integral_FTC_nonneg:
+lemma interval_integral_FTC_nonneg:
   fixes f F :: "real \<Rightarrow> real" and a b :: ereal
   assumes "a < b"
   assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV F x :> f x"
@@ -628,7 +628,7 @@
   shows
     "set_integrable lborel (einterval a b) f"
     "(LBINT x=a..b. f x) = B - A"
-proof%unimportant -
+proof -
   obtain u l where approx:
     "einterval a b = (\<Union>i. {l i .. u i})"
     "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
@@ -669,7 +669,7 @@
     by (rule interval_integral_Icc_approx_nonneg [OF \<open>a < b\<close> approx 1 f_nonneg 2 3])
 qed
 
-lemma%important interval_integral_FTC_integrable:
+theorem interval_integral_FTC_integrable:
   fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: ereal
   assumes "a < b"
   assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> (F has_vector_derivative f x) (at x)"
@@ -678,7 +678,7 @@
   assumes A: "((F \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)"
   assumes B: "((F \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
   shows "(LBINT x=a..b. f x) = B - A"
-proof%unimportant -
+proof -
   obtain u l where approx:
     "einterval a b = (\<Union>i. {l i .. u i})"
     "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
@@ -714,14 +714,14 @@
   einterval.
 *)
 
-lemma%important interval_integral_FTC2:
+theorem interval_integral_FTC2:
   fixes a b c :: real and f :: "real \<Rightarrow> 'a::euclidean_space"
   assumes "a \<le> c" "c \<le> b"
   and contf: "continuous_on {a..b} f"
   fixes x :: real
   assumes "a \<le> x" and "x \<le> b"
   shows "((\<lambda>u. LBINT y=c..u. f y) has_vector_derivative (f x)) (at x within {a..b})"
-proof%unimportant -
+proof -
   let ?F = "(\<lambda>u. LBINT y=a..u. f y)"
   have intf: "set_integrable lborel {a..b} f"
     by (rule borel_integrable_atLeastAtMost', rule contf)
@@ -746,11 +746,11 @@
   qed (insert assms, auto)
 qed
 
-lemma%important einterval_antiderivative:
+proposition einterval_antiderivative:
   fixes a b :: ereal and f :: "real \<Rightarrow> 'a::euclidean_space"
   assumes "a < b" and contf: "\<And>x :: real. a < x \<Longrightarrow> x < b \<Longrightarrow> isCont f x"
   shows "\<exists>F. \<forall>x :: real. a < x \<longrightarrow> x < b \<longrightarrow> (F has_vector_derivative f x) (at x)"
-proof%unimportant -
+proof -
   from einterval_nonempty [OF \<open>a < b\<close>] obtain c :: real where [simp]: "a < c" "c < b"
     by (auto simp: einterval_def)
   let ?F = "(\<lambda>u. LBINT y=c..u. f y)"
@@ -786,14 +786,14 @@
 text\<open>Once again, three versions: first, for finite intervals, and then two versions for
     arbitrary intervals.\<close>
 
-lemma%important interval_integral_substitution_finite:
+theorem interval_integral_substitution_finite:
   fixes a b :: real and f :: "real \<Rightarrow> 'a::euclidean_space"
   assumes "a \<le> b"
   and derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_real_derivative (g' x)) (at x within {a..b})"
   and contf : "continuous_on (g ` {a..b}) f"
   and contg': "continuous_on {a..b} g'"
   shows "LBINT x=a..b. g' x *\<^sub>R f (g x) = LBINT y=g a..g b. f y"
-proof%unimportant-
+proof-
   have v_derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_vector_derivative (g' x)) (at x within {a..b})"
     using derivg unfolding has_field_derivative_iff_has_vector_derivative .
   then have contg [simp]: "continuous_on {a..b} g"
@@ -833,7 +833,7 @@
 
 (* TODO: is it possible to lift the assumption here that g' is nonnegative? *)
 
-lemma%important interval_integral_substitution_integrable:
+theorem interval_integral_substitution_integrable:
   fixes f :: "real \<Rightarrow> 'a::euclidean_space" and a b u v :: ereal
   assumes "a < b"
   and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x"
@@ -845,7 +845,7 @@
   and integrable: "set_integrable lborel (einterval a b) (\<lambda>x. g' x *\<^sub>R f (g x))"
   and integrable2: "set_integrable lborel (einterval A B) (\<lambda>x. f x)"
   shows "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))"
-proof%unimportant -
+proof -
   obtain u l where approx [simp]:
     "einterval a b = (\<Union>i. {l i .. u i})"
     "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
@@ -932,7 +932,7 @@
    An alternative: make the second one the main one, and then have another lemma
    that says that if f is nonnegative and all the other hypotheses hold, then it is integrable. *)
 
-lemma%important interval_integral_substitution_nonneg:
+theorem interval_integral_substitution_nonneg:
   fixes f g g':: "real \<Rightarrow> real" and a b u v :: ereal
   assumes "a < b"
   and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x"
@@ -946,7 +946,7 @@
   shows
     "set_integrable lborel (einterval A B) f"
     "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))"
-proof%unimportant -
+proof -
   from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx [simp] = this
   note less_imp_le [simp]
   have aless[simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
@@ -1079,17 +1079,17 @@
 translations
   "CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
 
-lemma%important interval_integral_norm:
+proposition interval_integral_norm:
   fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
   shows "interval_lebesgue_integrable lborel a b f \<Longrightarrow> a \<le> b \<Longrightarrow>
     norm (LBINT t=a..b. f t) \<le> LBINT t=a..b. norm (f t)"
   using%unimportant integral_norm_bound[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
   by%unimportant (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)
 
-lemma%important interval_integral_norm2:
+proposition interval_integral_norm2:
   "interval_lebesgue_integrable lborel a b f \<Longrightarrow>
     norm (LBINT t=a..b. f t) \<le> \<bar>LBINT t=a..b. norm (f t)\<bar>"
-proof%unimportant (induct a b rule: linorder_wlog)
+proof (induct a b rule: linorder_wlog)
   case (sym a b) then show ?case
     by (simp add: interval_integral_endpoints_reverse[of a b] interval_integrable_endpoints_reverse[of a b])
 next