# HG changeset patch
# User Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
# Date 1548289709 0
# Node ID 0c3dcb3a17f68a2c75adc888354c0194b7d6a3e2
# Parent  2444c8b85aac09b8dc43563886130b79b56ba583
tagged 5 theories

diff -r 2444c8b85aac -r 0c3dcb3a17f6 src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Wed Jan 23 17:20:35 2019 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Thu Jan 24 00:28:29 2019 +0000
@@ -1,4 +1,4 @@
-subsection \<open>Ordered Euclidean Space\<close>
+subsection \<open>Ordered Euclidean Space\<close> (* why not Section? *)
 
 theory Ordered_Euclidean_Space
 imports
@@ -6,7 +6,7 @@
   "HOL-Library.Product_Order"
 begin
 
-text%important \<open>An ordering on euclidean spaces that will allow us to talk about intervals\<close>
+text \<open>An ordering on euclidean spaces that will allow us to talk about intervals\<close>
 
 class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space +
   assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)"
@@ -35,7 +35,7 @@
   by standard (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI)
 
 subclass conditionally_complete_lattice
-proof%unimportant
+proof
   fix z::'a and X::"'a set"
   assume "X \<noteq> {}"
   hence "\<And>i. (\<lambda>x. x \<bullet> i) ` X \<noteq> {}" by simp
@@ -46,42 +46,42 @@
       simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def
         eucl_Inf eucl_Sup eucl_le)+
 
-lemma%unimportant inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)"
+lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)"
   and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)"
   by (simp_all add: eucl_inf eucl_sup inner_sum_left inner_Basis if_distrib comm_monoid_add_class.sum.delta
       cong: if_cong)
 
-lemma%unimportant inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x\<in>X. f x) \<bullet> i = (INF x\<in>X. f x \<bullet> i)"
+lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x\<in>X. f x) \<bullet> i = (INF x\<in>X. f x \<bullet> i)"
   and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x\<in>X. f x) \<bullet> i = (SUP x\<in>X. f x \<bullet> i)"
   using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def)
 
-lemma%unimportant abs_inner: "i \<in> Basis \<Longrightarrow> \<bar>x\<bar> \<bullet> i = \<bar>x \<bullet> i\<bar>"
+lemma abs_inner: "i \<in> Basis \<Longrightarrow> \<bar>x\<bar> \<bullet> i = \<bar>x \<bullet> i\<bar>"
   by (auto simp: eucl_abs)
 
-lemma%unimportant
+lemma
   abs_scaleR: "\<bar>a *\<^sub>R b\<bar> = \<bar>a\<bar> *\<^sub>R \<bar>b\<bar>"
   by (auto simp: eucl_abs abs_mult intro!: euclidean_eqI)
 
-lemma%unimportant interval_inner_leI:
+lemma interval_inner_leI:
   assumes "x \<in> {a .. b}" "0 \<le> i"
   shows "a\<bullet>i \<le> x\<bullet>i" "x\<bullet>i \<le> b\<bullet>i"
   using assms
   unfolding euclidean_inner[of a i] euclidean_inner[of x i] euclidean_inner[of b i]
   by (auto intro!: ordered_comm_monoid_add_class.sum_mono mult_right_mono simp: eucl_le)
 
-lemma%unimportant inner_nonneg_nonneg:
+lemma inner_nonneg_nonneg:
   shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a \<bullet> b"
   using interval_inner_leI[of a 0 a b]
   by auto
 
-lemma%unimportant inner_Basis_mono:
+lemma inner_Basis_mono:
   shows "a \<le> b \<Longrightarrow> c \<in> Basis  \<Longrightarrow> a \<bullet> c \<le> b \<bullet> c"
   by (simp add: eucl_le)
 
-lemma%unimportant Basis_nonneg[intro, simp]: "i \<in> Basis \<Longrightarrow> 0 \<le> i"
+lemma Basis_nonneg[intro, simp]: "i \<in> Basis \<Longrightarrow> 0 \<le> i"
   by (auto simp: eucl_le inner_Basis)
 
-lemma%unimportant Sup_eq_maximum_componentwise:
+lemma Sup_eq_maximum_componentwise:
   fixes s::"'a set"
   assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b"
   assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> x \<bullet> b \<le> X \<bullet> b"
@@ -91,7 +91,7 @@
   unfolding eucl_Sup euclidean_representation_sum
   by (auto intro!: conditionally_complete_lattice_class.cSup_eq_maximum)
 
-lemma%unimportant Inf_eq_minimum_componentwise:
+lemma Inf_eq_minimum_componentwise:
   assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b"
   assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> X \<bullet> b \<le> x \<bullet> b"
   assumes i_s: "\<And>b. b \<in> Basis \<Longrightarrow> (i b \<bullet> b) \<in> (\<lambda>x. x \<bullet> b) ` s"
@@ -102,12 +102,11 @@
 
 end
 
-lemma%important
-  compact_attains_Inf_componentwise:
+proposition  compact_attains_Inf_componentwise:
   fixes b::"'a::ordered_euclidean_space"
   assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X"
   obtains x where "x \<in> X" "x \<bullet> b = Inf X \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b"
-proof%unimportant atomize_elim
+proof atomize_elim
   let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
   from assms have "compact ?proj" "?proj \<noteq> {}"
     by (auto intro!: compact_continuous_image continuous_intros)
@@ -124,12 +123,12 @@
   with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Inf X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> x \<bullet> b \<le> y \<bullet> b)" by blast
 qed
 
-lemma%important
+proposition
   compact_attains_Sup_componentwise:
   fixes b::"'a::ordered_euclidean_space"
   assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X"
   obtains x where "x \<in> X" "x \<bullet> b = Sup X \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b"
-proof%unimportant atomize_elim
+proof atomize_elim
   let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
   from assms have "compact ?proj" "?proj \<noteq> {}"
     by (auto intro!: compact_continuous_image continuous_intros)
@@ -146,19 +145,19 @@
   with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Sup X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> y \<bullet> b \<le> x \<bullet> b)" by blast
 qed
 
-lemma%unimportant (in order) atLeastatMost_empty'[simp]:
+lemma (in order) atLeastatMost_empty'[simp]:
   "(\<not> a \<le> b) \<Longrightarrow> {a..b} = {}"
   by (auto)
 
 instance real :: ordered_euclidean_space
   by standard auto
 
-lemma%unimportant in_Basis_prod_iff:
+lemma in_Basis_prod_iff:
   fixes i::"'a::euclidean_space*'b::euclidean_space"
   shows "i \<in> Basis \<longleftrightarrow> fst i = 0 \<and> snd i \<in> Basis \<or> snd i = 0 \<and> fst i \<in> Basis"
   by (cases i) (auto simp: Basis_prod_def)
 
-instantiation prod :: (abs, abs) abs
+instantiation%unimportant prod :: (abs, abs) abs
 begin
 
 definition "\<bar>x\<bar> = (\<bar>fst x\<bar>, \<bar>snd x\<bar>)"
@@ -176,52 +175,52 @@
 
 text\<open>Instantiation for intervals on \<open>ordered_euclidean_space\<close>\<close>
 
-lemma%important
+proposition
   fixes a :: "'a::ordered_euclidean_space"
   shows cbox_interval: "cbox a b = {a..b}"
     and interval_cbox: "{a..b} = cbox a b"
     and eucl_le_atMost: "{x. \<forall>i\<in>Basis. x \<bullet> i <= a \<bullet> i} = {..a}"
     and eucl_le_atLeast: "{x. \<forall>i\<in>Basis. a \<bullet> i <= x \<bullet> i} = {a..}"
-    by%unimportant (auto simp: eucl_le[where 'a='a] eucl_less_def box_def cbox_def)
+  by (auto simp: eucl_le[where 'a='a] eucl_less_def box_def cbox_def)
 
-lemma%unimportant vec_nth_real_1_iff_cbox [simp]:
+lemma vec_nth_real_1_iff_cbox [simp]:
   fixes a b :: real
   shows "(\<lambda>x::real^1. x $ 1) ` S = {a..b} \<longleftrightarrow> S = cbox (vec a) (vec b)"
   by (metis interval_cbox vec_nth_1_iff_cbox)
 
-lemma%unimportant closed_eucl_atLeastAtMost[simp, intro]:
+lemma closed_eucl_atLeastAtMost[simp, intro]:
   fixes a :: "'a::ordered_euclidean_space"
   shows "closed {a..b}"
   by (simp add: cbox_interval[symmetric] closed_cbox)
 
-lemma%unimportant closed_eucl_atMost[simp, intro]:
+lemma closed_eucl_atMost[simp, intro]:
   fixes a :: "'a::ordered_euclidean_space"
   shows "closed {..a}"
   by (simp add: closed_interval_left eucl_le_atMost[symmetric])
 
-lemma%unimportant closed_eucl_atLeast[simp, intro]:
+lemma closed_eucl_atLeast[simp, intro]:
   fixes a :: "'a::ordered_euclidean_space"
   shows "closed {a..}"
   by (simp add: closed_interval_right eucl_le_atLeast[symmetric])
 
-lemma%unimportant bounded_closed_interval [simp]:
+lemma bounded_closed_interval [simp]:
   fixes a :: "'a::ordered_euclidean_space"
   shows "bounded {a .. b}"
   using bounded_cbox[of a b]
   by (metis interval_cbox)
 
-lemma%unimportant convex_closed_interval [simp]:
+lemma convex_closed_interval [simp]:
   fixes a :: "'a::ordered_euclidean_space"
   shows "convex {a .. b}"
   using convex_box[of a b]
   by (metis interval_cbox)
 
-lemma%unimportant image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a .. b} =
+lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a .. b} =
   (if {a .. b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a .. m *\<^sub>R b} else {m *\<^sub>R b .. m *\<^sub>R a})"
   using image_smult_cbox[of m a b]
   by (simp add: cbox_interval)
 
-lemma%unimportant [simp]:
+lemma [simp]:
   fixes a b::"'a::ordered_euclidean_space" and r s::real
   shows is_interval_io: "is_interval {..<r}"
     and is_interval_ic: "is_interval {..a}"
@@ -243,15 +242,15 @@
   shows "path_connected {a..b}"
   using is_interval_cc is_interval_path_connected by blast
 
-lemma%unimportant is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
+lemma is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
   by (auto simp: real_atLeastGreaterThan_eq)
 
-lemma%unimportant compact_interval [simp]:
+lemma compact_interval [simp]:
   fixes a b::"'a::ordered_euclidean_space"
   shows "compact {a .. b}"
   by (metis compact_cbox interval_cbox)
 
-lemma%unimportant homeomorphic_closed_intervals:
+lemma homeomorphic_closed_intervals:
   fixes a :: "'a::euclidean_space" and b and c :: "'a::euclidean_space" and d
   assumes "box a b \<noteq> {}" and "box c d \<noteq> {}"
     shows "(cbox a b) homeomorphic (cbox c d)"
@@ -259,7 +258,7 @@
 using assms apply auto
 done
 
-lemma%unimportant homeomorphic_closed_intervals_real:
+lemma homeomorphic_closed_intervals_real:
   fixes a::real and b and c::real and d
   assumes "a<b" and "c<d"
   shows "{a..b} homeomorphic {c..d}"
@@ -268,10 +267,10 @@
 no_notation
   eucl_less (infix "<e" 50)
 
-lemma%unimportant One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)"
+lemma One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)"
   by (auto intro: sum_nonneg)
 
-lemma%unimportant
+lemma
   fixes a b::"'a::ordered_euclidean_space"
   shows bdd_above_cbox[intro, simp]: "bdd_above (cbox a b)"
     and bdd_below_cbox[intro, simp]: "bdd_below (cbox a b)"
@@ -300,12 +299,12 @@
 
 end
 
-lemma%unimportant ANR_interval [iff]:
+lemma ANR_interval [iff]:
     fixes a :: "'a::ordered_euclidean_space"
     shows "ANR{a..b}"
 by (simp add: interval_cbox)
 
-lemma%unimportant ENR_interval [iff]:
+lemma ENR_interval [iff]:
     fixes a :: "'a::ordered_euclidean_space"
     shows "ENR{a..b}"
   by (auto simp: interval_cbox)
diff -r 2444c8b85aac -r 0c3dcb3a17f6 src/HOL/Analysis/Poly_Roots.thy
--- a/src/HOL/Analysis/Poly_Roots.thy	Wed Jan 23 17:20:35 2019 +0100
+++ b/src/HOL/Analysis/Poly_Roots.thy	Thu Jan 24 00:28:29 2019 +0000
@@ -2,7 +2,7 @@
     Ported from "hol_light/Multivariate/complexes.ml" by L C Paulson
 *)
 
-section%important \<open>Polynomial Functions: Extremal Behaviour and Root Counts\<close>
+section \<open>Polynomial Functions: Extremal Behaviour and Root Counts\<close>
 
 theory Poly_Roots
 imports Complex_Main
@@ -10,11 +10,11 @@
 
 subsection\<open>Basics about polynomial functions: extremal behaviour and root counts\<close>
 
-lemma%important sub_polyfun:
+lemma sub_polyfun:
   fixes x :: "'a::{comm_ring,monoid_mult}"
   shows   "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
            (x - y) * (\<Sum>j<n. \<Sum>k= Suc j..n. a k * y^(k - Suc j) * x^j)"
-proof%unimportant -
+proof -
   have "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
         (\<Sum>i\<le>n. a i * (x^i - y^i))"
     by (simp add: algebra_simps sum_subtractf [symmetric])
@@ -27,7 +27,7 @@
   finally show ?thesis .
 qed
 
-lemma%unimportant sub_polyfun_alt:
+lemma sub_polyfun_alt:
   fixes x :: "'a::{comm_ring,monoid_mult}"
   shows   "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
            (x - y) * (\<Sum>j<n. \<Sum>k<n-j. a (j+k+1) * y^k * x^j)"
@@ -40,7 +40,7 @@
     by (simp add: sub_polyfun)
 qed
 
-lemma%unimportant polyfun_linear_factor:
+lemma polyfun_linear_factor:
   fixes a :: "'a::{comm_ring,monoid_mult}"
   shows  "\<exists>b. \<forall>z. (\<Sum>i\<le>n. c i * z^i) =
                   (z-a) * (\<Sum>i<n. b i * z^i) + (\<Sum>i\<le>n. c i * a^i)"
@@ -57,21 +57,21 @@
     by (intro exI allI)
 qed
 
-lemma%important polyfun_linear_factor_root:
+lemma polyfun_linear_factor_root:
   fixes a :: "'a::{comm_ring,monoid_mult}"
   assumes "(\<Sum>i\<le>n. c i * a^i) = 0"
   shows  "\<exists>b. \<forall>z. (\<Sum>i\<le>n. c i * z^i) = (z-a) * (\<Sum>i<n. b i * z^i)"
-  using%unimportant polyfun_linear_factor [of c n a] assms
-  by%unimportant simp
+  using polyfun_linear_factor [of c n a] assms
+  by simp
 
-lemma%unimportant adhoc_norm_triangle: "a + norm(y) \<le> b ==> norm(x) \<le> a ==> norm(x + y) \<le> b"
+lemma adhoc_norm_triangle: "a + norm(y) \<le> b ==> norm(x) \<le> a ==> norm(x + y) \<le> b"
   by (metis norm_triangle_mono order.trans order_refl)
 
-lemma%important polyfun_extremal_lemma:
+proposition polyfun_extremal_lemma:
   fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
   assumes "e > 0"
     shows "\<exists>M. \<forall>z. M \<le> norm z \<longrightarrow> norm(\<Sum>i\<le>n. c i * z^i) \<le> e * norm(z) ^ Suc n"
-proof%unimportant (induction n)
+proof (induction n)
   case 0
   show ?case
     by (rule exI [where x="norm (c 0) / e"]) (auto simp: mult.commute pos_divide_le_eq assms)
@@ -102,7 +102,7 @@
     qed
 qed
 
-lemma%unimportant norm_lemma_xy: assumes "\<bar>b\<bar> + 1 \<le> norm(y) - a" "norm(x) \<le> a" shows "b \<le> norm(x + y)"
+lemma norm_lemma_xy: assumes "\<bar>b\<bar> + 1 \<le> norm(y) - a" "norm(x) \<le> a" shows "b \<le> norm(x + y)"
 proof -
   have "b \<le> norm y - norm x"
     using assms by linarith
@@ -110,12 +110,12 @@
     by (metis (no_types) add.commute norm_diff_ineq order_trans)
 qed
 
-lemma%important polyfun_extremal:
+proposition polyfun_extremal:
   fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
   assumes "\<exists>k. k \<noteq> 0 \<and> k \<le> n \<and> c k \<noteq> 0"
     shows "eventually (\<lambda>z. norm(\<Sum>i\<le>n. c i * z^i) \<ge> B) at_infinity"
 using assms
-proof%unimportant (induction n)
+proof (induction n)
   case 0 then show ?case
     by simp
 next
@@ -149,12 +149,12 @@
   qed
 qed
 
-lemma%important polyfun_rootbound:
+proposition polyfun_rootbound:
  fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
  assumes "\<exists>k. k \<le> n \<and> c k \<noteq> 0"
    shows "finite {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<and> card {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<le> n"
 using assms
-proof%unimportant (induction n arbitrary: c)
+proof (induction n arbitrary: c)
  case (Suc n) show ?case
  proof (cases "{z. (\<Sum>i\<le>Suc n. c i * z^i) = 0} = {}")
    case False
@@ -182,17 +182,17 @@
    qed simp
 qed simp
 
-corollary%important (*FIX ME needs name *)
+corollary (*FIX ME needs name *)
   fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
   assumes "\<exists>k. k \<le> n \<and> c k \<noteq> 0"
     shows polyfun_rootbound_finite: "finite {z. (\<Sum>i\<le>n. c i * z^i) = 0}"
       and polyfun_rootbound_card:   "card {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<le> n"
 using polyfun_rootbound [OF assms] by auto
 
-lemma%important polyfun_finite_roots:
+proposition polyfun_finite_roots:
   fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
     shows  "finite {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<longleftrightarrow> (\<exists>k. k \<le> n \<and> c k \<noteq> 0)"
-proof%unimportant (cases " \<exists>k\<le>n. c k \<noteq> 0")
+proof (cases " \<exists>k\<le>n. c k \<noteq> 0")
   case True then show ?thesis
     by (blast intro: polyfun_rootbound_finite)
 next
@@ -200,7 +200,7 @@
     by (auto simp: infinite_UNIV_char_0)
 qed
 
-lemma%unimportant polyfun_eq_0:
+lemma polyfun_eq_0:
   fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
     shows  "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = 0) \<longleftrightarrow> (\<forall>k. k \<le> n \<longrightarrow> c k = 0)"
 proof (cases "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = 0)")
@@ -215,10 +215,10 @@
     by auto
 qed
 
-lemma%important polyfun_eq_const:
+theorem polyfun_eq_const:
   fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
     shows  "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = k) \<longleftrightarrow> c 0 = k \<and> (\<forall>k. k \<noteq> 0 \<and> k \<le> n \<longrightarrow> c k = 0)"
-proof%unimportant -
+proof -
   {fix z
     have "(\<Sum>i\<le>n. c i * z^i) = (\<Sum>i\<le>n. (if i = 0 then c 0 - k else c i) * z^i) + k"
       by (induct n) auto
diff -r 2444c8b85aac -r 0c3dcb3a17f6 src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Wed Jan 23 17:20:35 2019 +0100
+++ b/src/HOL/Analysis/Polytope.thy	Thu Jan 24 00:28:29 2019 +0000
@@ -14,10 +14,10 @@
         T \<subseteq> S \<and> convex T \<and>
         (\<forall>a \<in> S. \<forall>b \<in> S. \<forall>x \<in> T. x \<in> open_segment a b \<longrightarrow> a \<in> T \<and> b \<in> T)"
 
-lemma%unimportant face_ofD: "\<lbrakk>T face_of S; x \<in> open_segment a b; a \<in> S; b \<in> S; x \<in> T\<rbrakk> \<Longrightarrow> a \<in> T \<and> b \<in> T"
+lemma face_ofD: "\<lbrakk>T face_of S; x \<in> open_segment a b; a \<in> S; b \<in> S; x \<in> T\<rbrakk> \<Longrightarrow> a \<in> T \<and> b \<in> T"
   unfolding face_of_def by blast
 
-lemma%unimportant face_of_translation_eq [simp]:
+lemma face_of_translation_eq [simp]:
     "((+) a ` T face_of (+) a ` S) \<longleftrightarrow> T face_of S"
 proof -
   have *: "\<And>a T S. T face_of S \<Longrightarrow> ((+) a ` T face_of (+) a ` S)"
@@ -32,52 +32,52 @@
     done
 qed
 
-lemma%unimportant face_of_linear_image:
+lemma face_of_linear_image:
   assumes "linear f" "inj f"
     shows "(f ` c face_of f ` S) \<longleftrightarrow> c face_of S"
 by (simp add: face_of_def inj_image_subset_iff inj_image_mem_iff open_segment_linear_image assms)
 
-lemma%unimportant face_of_refl: "convex S \<Longrightarrow> S face_of S"
+lemma face_of_refl: "convex S \<Longrightarrow> S face_of S"
   by (auto simp: face_of_def)
 
-lemma%unimportant face_of_refl_eq: "S face_of S \<longleftrightarrow> convex S"
+lemma face_of_refl_eq: "S face_of S \<longleftrightarrow> convex S"
   by (auto simp: face_of_def)
 
-lemma%unimportant empty_face_of [iff]: "{} face_of S"
+lemma empty_face_of [iff]: "{} face_of S"
   by (simp add: face_of_def)
 
-lemma%unimportant face_of_empty [simp]: "S face_of {} \<longleftrightarrow> S = {}"
+lemma face_of_empty [simp]: "S face_of {} \<longleftrightarrow> S = {}"
   by (meson empty_face_of face_of_def subset_empty)
 
-lemma%unimportant face_of_trans [trans]: "\<lbrakk>S face_of T; T face_of u\<rbrakk> \<Longrightarrow> S face_of u"
+lemma face_of_trans [trans]: "\<lbrakk>S face_of T; T face_of u\<rbrakk> \<Longrightarrow> S face_of u"
   unfolding face_of_def by (safe; blast)
 
-lemma%unimportant face_of_face: "T face_of S \<Longrightarrow> (f face_of T \<longleftrightarrow> f face_of S \<and> f \<subseteq> T)"
+lemma face_of_face: "T face_of S \<Longrightarrow> (f face_of T \<longleftrightarrow> f face_of S \<and> f \<subseteq> T)"
   unfolding face_of_def by (safe; blast)
 
-lemma%unimportant face_of_subset: "\<lbrakk>F face_of S; F \<subseteq> T; T \<subseteq> S\<rbrakk> \<Longrightarrow> F face_of T"
+lemma face_of_subset: "\<lbrakk>F face_of S; F \<subseteq> T; T \<subseteq> S\<rbrakk> \<Longrightarrow> F face_of T"
   unfolding face_of_def by (safe; blast)
 
-lemma%unimportant face_of_slice: "\<lbrakk>F face_of S; convex T\<rbrakk> \<Longrightarrow> (F \<inter> T) face_of (S \<inter> T)"
+lemma face_of_slice: "\<lbrakk>F face_of S; convex T\<rbrakk> \<Longrightarrow> (F \<inter> T) face_of (S \<inter> T)"
   unfolding face_of_def by (blast intro: convex_Int)
 
-lemma%unimportant face_of_Int: "\<lbrakk>t1 face_of S; t2 face_of S\<rbrakk> \<Longrightarrow> (t1 \<inter> t2) face_of S"
+lemma face_of_Int: "\<lbrakk>t1 face_of S; t2 face_of S\<rbrakk> \<Longrightarrow> (t1 \<inter> t2) face_of S"
   unfolding face_of_def by (blast intro: convex_Int)
 
-lemma%unimportant face_of_Inter: "\<lbrakk>A \<noteq> {}; \<And>T. T \<in> A \<Longrightarrow> T face_of S\<rbrakk> \<Longrightarrow> (\<Inter> A) face_of S"
+lemma face_of_Inter: "\<lbrakk>A \<noteq> {}; \<And>T. T \<in> A \<Longrightarrow> T face_of S\<rbrakk> \<Longrightarrow> (\<Inter> A) face_of S"
   unfolding face_of_def by (blast intro: convex_Inter)
 
-lemma%unimportant face_of_Int_Int: "\<lbrakk>F face_of T; F' face_of t'\<rbrakk> \<Longrightarrow> (F \<inter> F') face_of (T \<inter> t')"
+lemma face_of_Int_Int: "\<lbrakk>F face_of T; F' face_of t'\<rbrakk> \<Longrightarrow> (F \<inter> F') face_of (T \<inter> t')"
   unfolding face_of_def by (blast intro: convex_Int)
 
-lemma%unimportant face_of_imp_subset: "T face_of S \<Longrightarrow> T \<subseteq> S"
+lemma face_of_imp_subset: "T face_of S \<Longrightarrow> T \<subseteq> S"
   unfolding face_of_def by blast
 
-lemma%important face_of_imp_eq_affine_Int:
+proposition face_of_imp_eq_affine_Int:
   fixes S :: "'a::euclidean_space set"
   assumes S: "convex S"  and T: "T face_of S"
   shows "T = (affine hull T) \<inter> S"
-proof%unimportant -
+proof -
   have "convex T" using T by (simp add: face_of_def)
   have *: False if x: "x \<in> affine hull T" and "x \<in> S" "x \<notin> T" and y: "y \<in> rel_interior T" for x y
   proof -
@@ -114,15 +114,15 @@
     done
 qed
 
-lemma%unimportant face_of_imp_closed:
+lemma face_of_imp_closed:
      fixes S :: "'a::euclidean_space set"
      assumes "convex S" "closed S" "T face_of S" shows "closed T"
   by (metis affine_affine_hull affine_closed closed_Int face_of_imp_eq_affine_Int assms)
 
-lemma%important face_of_Int_supporting_hyperplane_le_strong:
+lemma face_of_Int_supporting_hyperplane_le_strong:
     assumes "convex(S \<inter> {x. a \<bullet> x = b})" and aleb: "\<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b"
       shows "(S \<inter> {x. a \<bullet> x = b}) face_of S"
-proof%unimportant -
+proof -
   have *: "a \<bullet> u = a \<bullet> x" if "x \<in> open_segment u v" "u \<in> S" "v \<in> S" and b: "b = a \<bullet> x"
           for u v x
   proof (rule antisym)
@@ -145,33 +145,33 @@
     using "*" open_segment_commute by blast
 qed
 
-lemma%unimportant face_of_Int_supporting_hyperplane_ge_strong:
+lemma face_of_Int_supporting_hyperplane_ge_strong:
    "\<lbrakk>convex(S \<inter> {x. a \<bullet> x = b}); \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk>
     \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) face_of S"
   using face_of_Int_supporting_hyperplane_le_strong [of S "-a" "-b"] by simp
 
-lemma%unimportant face_of_Int_supporting_hyperplane_le:
+lemma face_of_Int_supporting_hyperplane_le:
     "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) face_of S"
   by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_le_strong)
 
-lemma%unimportant face_of_Int_supporting_hyperplane_ge:
+lemma face_of_Int_supporting_hyperplane_ge:
     "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) face_of S"
   by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_ge_strong)
 
-lemma%unimportant face_of_imp_convex: "T face_of S \<Longrightarrow> convex T"
+lemma face_of_imp_convex: "T face_of S \<Longrightarrow> convex T"
   using face_of_def by blast
 
-lemma%unimportant face_of_imp_compact:
+lemma face_of_imp_compact:
     fixes S :: "'a::euclidean_space set"
     shows "\<lbrakk>convex S; compact S; T face_of S\<rbrakk> \<Longrightarrow> compact T"
   by (meson bounded_subset compact_eq_bounded_closed face_of_imp_closed face_of_imp_subset)
 
-lemma%unimportant face_of_Int_subface:
+lemma face_of_Int_subface:
      "\<lbrakk>A \<inter> B face_of A; A \<inter> B face_of B; C face_of A; D face_of B\<rbrakk>
       \<Longrightarrow> (C \<inter> D) face_of C \<and> (C \<inter> D) face_of D"
   by (meson face_of_Int_Int face_of_face inf_le1 inf_le2)
 
-lemma%unimportant subset_of_face_of:
+lemma subset_of_face_of:
     fixes S :: "'a::real_normed_vector set"
     assumes "T face_of S" "u \<subseteq> S" "T \<inter> (rel_interior u) \<noteq> {}"
       shows "u \<subseteq> T"
@@ -213,7 +213,7 @@
   qed
 qed
 
-lemma%unimportant face_of_eq:
+lemma face_of_eq:
     fixes S :: "'a::real_normed_vector set"
     assumes "T face_of S" "u face_of S" "(rel_interior T) \<inter> (rel_interior u) \<noteq> {}"
       shows "T = u"
@@ -221,13 +221,13 @@
   apply (metis assms disjoint_iff_not_equal face_of_imp_subset rel_interior_subset subsetCE subset_of_face_of)
   by (metis assms disjoint_iff_not_equal face_of_imp_subset rel_interior_subset subset_iff subset_of_face_of)
 
-lemma%unimportant face_of_disjoint_rel_interior:
+lemma face_of_disjoint_rel_interior:
       fixes S :: "'a::real_normed_vector set"
       assumes "T face_of S" "T \<noteq> S"
         shows "T \<inter> rel_interior S = {}"
   by (meson assms subset_of_face_of face_of_imp_subset order_refl subset_antisym)
 
-lemma%unimportant face_of_disjoint_interior:
+lemma face_of_disjoint_interior:
       fixes S :: "'a::real_normed_vector set"
       assumes "T face_of S" "T \<noteq> S"
         shows "T \<inter> interior S = {}"
@@ -238,19 +238,19 @@
     by (metis (no_types) Int_greatest assms face_of_disjoint_rel_interior inf_sup_ord(1) subset_empty)
 qed
 
-lemma%unimportant face_of_subset_rel_boundary:
+lemma face_of_subset_rel_boundary:
   fixes S :: "'a::real_normed_vector set"
   assumes "T face_of S" "T \<noteq> S"
     shows "T \<subseteq> (S - rel_interior S)"
 by (meson DiffI assms disjoint_iff_not_equal face_of_disjoint_rel_interior face_of_imp_subset rev_subsetD subsetI)
 
-lemma%unimportant face_of_subset_rel_frontier:
+lemma face_of_subset_rel_frontier:
     fixes S :: "'a::real_normed_vector set"
     assumes "T face_of S" "T \<noteq> S"
       shows "T \<subseteq> rel_frontier S"
   using assms closure_subset face_of_disjoint_rel_interior face_of_imp_subset rel_frontier_def by fastforce
 
-lemma%unimportant face_of_aff_dim_lt:
+lemma face_of_aff_dim_lt:
   fixes S :: "'a::euclidean_space set"
   assumes "convex S" "T face_of S" "T \<noteq> S"
     shows "aff_dim T < aff_dim S"
@@ -268,7 +268,7 @@
     by simp
 qed
 
-lemma%unimportant subset_of_face_of_affine_hull:
+lemma subset_of_face_of_affine_hull:
     fixes S :: "'a::euclidean_space set"
   assumes T: "T face_of S" and "convex S" "U \<subseteq> S" and dis: "\<not> disjnt (affine hull T) (rel_interior U)"
   shows "U \<subseteq> T"
@@ -277,13 +277,13 @@
   using rel_interior_subset [of U] dis
   using \<open>U \<subseteq> S\<close> disjnt_def by fastforce
 
-lemma%unimportant affine_hull_face_of_disjoint_rel_interior:
+lemma affine_hull_face_of_disjoint_rel_interior:
     fixes S :: "'a::euclidean_space set"
   assumes "convex S" "F face_of S" "F \<noteq> S"
   shows "affine hull F \<inter> rel_interior S = {}"
   by (metis assms disjnt_def face_of_imp_subset order_refl subset_antisym subset_of_face_of_affine_hull)
 
-lemma%unimportant affine_diff_divide:
+lemma affine_diff_divide:
     assumes "affine S" "k \<noteq> 0" "k \<noteq> 1" and xy: "x \<in> S" "y /\<^sub>R (1 - k) \<in> S"
       shows "(x - y) /\<^sub>R k \<in> S"
 proof -
@@ -294,10 +294,10 @@
     using \<open>affine S\<close> xy by (auto simp: affine_alt)
 qed
 
-lemma%important face_of_convex_hulls:
+proposition face_of_convex_hulls:
       assumes S: "finite S" "T \<subseteq> S" and disj: "affine hull T \<inter> convex hull (S - T) = {}"
       shows  "(convex hull T) face_of (convex hull S)"
-proof%unimportant -
+proof -
   have fin: "finite T" "finite (S - T)" using assms
     by (auto simp: finite_subset)
   have *: "x \<in> convex hull T"
@@ -391,16 +391,16 @@
     using open_segment_commute by (auto simp: face_of_def intro: *)
 qed
 
-proposition%important face_of_convex_hull_insert:
+proposition face_of_convex_hull_insert:
    "\<lbrakk>finite S; a \<notin> affine hull S; T face_of convex hull S\<rbrakk> \<Longrightarrow> T face_of convex hull insert a S"
   apply (rule face_of_trans, blast)
   apply (rule face_of_convex_hulls; force simp: insert_Diff_if)
   done
 
-proposition%important face_of_affine_trivial:
+proposition face_of_affine_trivial:
     assumes "affine S" "T face_of S"
     shows "T = {} \<or> T = S"
-proof%unimportant (rule ccontr, clarsimp)
+proof (rule ccontr, clarsimp)
   assume "T \<noteq> {}" "T \<noteq> S"
   then obtain a where "a \<in> T" by auto
   then have "a \<in> S"
@@ -430,16 +430,16 @@
 qed
 
 
-lemma%unimportant face_of_affine_eq:
+lemma face_of_affine_eq:
    "affine S \<Longrightarrow> (T face_of S \<longleftrightarrow> T = {} \<or> T = S)"
 using affine_imp_convex face_of_affine_trivial face_of_refl by auto
 
 
-lemma%important Inter_faces_finite_altbound:
+proposition Inter_faces_finite_altbound:
     fixes T :: "'a::euclidean_space set set"
     assumes cfaI: "\<And>c. c \<in> T \<Longrightarrow> c face_of S"
     shows "\<exists>F'. finite F' \<and> F' \<subseteq> T \<and> card F' \<le> DIM('a) + 2 \<and> \<Inter>F' = \<Inter>T"
-proof%unimportant (cases "\<forall>F'. finite F' \<and> F' \<subseteq> T \<and> card F' \<le> DIM('a) + 2 \<longrightarrow> (\<exists>c. c \<in> T \<and> c \<inter> (\<Inter>F') \<subset> (\<Inter>F'))")
+proof (cases "\<forall>F'. finite F' \<and> F' \<subseteq> T \<and> card F' \<le> DIM('a) + 2 \<longrightarrow> (\<exists>c. c \<in> T \<and> c \<inter> (\<Inter>F') \<subset> (\<Inter>F'))")
   case True
   then obtain c where c:
        "\<And>F'. \<lbrakk>finite F'; F' \<subseteq> T; card F' \<le> DIM('a) + 2\<rbrakk> \<Longrightarrow> c F' \<in> T \<and> c F' \<inter> (\<Inter>F') \<subset> (\<Inter>F')"
@@ -499,17 +499,17 @@
     by blast
 qed
 
-lemma%unimportant faces_of_translation:
+lemma faces_of_translation:
    "{F. F face_of image (\<lambda>x. a + x) S} = image (image (\<lambda>x. a + x)) {F. F face_of S}"
 apply (rule subset_antisym, clarify)
 apply (auto simp: image_iff)
 apply (metis face_of_imp_subset face_of_translation_eq subset_imageE)
 done
 
-proposition%important face_of_Times:
+proposition face_of_Times:
   assumes "F face_of S" and "F' face_of S'"
     shows "(F \<times> F') face_of (S \<times> S')"
-proof%unimportant -
+proof -
   have "F \<times> F' \<subseteq> S \<times> S'"
     using assms [unfolded face_of_def] by blast
   moreover
@@ -531,11 +531,11 @@
     unfolding face_of_def by blast
 qed
 
-corollary%important face_of_Times_decomp:
+corollary face_of_Times_decomp:
     fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
     shows "c face_of (S \<times> S') \<longleftrightarrow> (\<exists>F F'. F face_of S \<and> F' face_of S' \<and> c = F \<times> F')"
      (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume c: ?lhs
   show ?rhs
   proof (cases "c = {}")
@@ -582,13 +582,13 @@
   assume ?rhs with face_of_Times show ?lhs by auto
 qed
 
-lemma%unimportant face_of_Times_eq:
+lemma face_of_Times_eq:
     fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
     shows "(F \<times> F') face_of (S \<times> S') \<longleftrightarrow>
            F = {} \<or> F' = {} \<or> F face_of S \<and> F' face_of S'"
 by (auto simp: face_of_Times_decomp times_eq_iff)
 
-lemma%unimportant hyperplane_face_of_halfspace_le: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<le> b}"
+lemma hyperplane_face_of_halfspace_le: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<le> b}"
 proof -
   have "{x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x = b} = {x. a \<bullet> x = b}"
     by auto
@@ -596,7 +596,7 @@
   show ?thesis by auto
 qed
 
-lemma%unimportant hyperplane_face_of_halfspace_ge: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<ge> b}"
+lemma hyperplane_face_of_halfspace_ge: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<ge> b}"
 proof -
   have "{x. a \<bullet> x \<ge> b} \<inter> {x. a \<bullet> x = b} = {x. a \<bullet> x = b}"
     by auto
@@ -604,12 +604,12 @@
   show ?thesis by auto
 qed
 
-lemma%important face_of_halfspace_le:
+lemma face_of_halfspace_le:
   fixes a :: "'n::euclidean_space"
   shows "F face_of {x. a \<bullet> x \<le> b} \<longleftrightarrow>
          F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<le> b}"
      (is "?lhs = ?rhs")
-proof%unimportant (cases "a = 0")
+proof (cases "a = 0")
   case True then show ?thesis
     using face_of_affine_eq affine_UNIV by auto
 next
@@ -635,7 +635,7 @@
   qed
 qed
 
-lemma%unimportant face_of_halfspace_ge:
+lemma face_of_halfspace_ge:
   fixes a :: "'n::euclidean_space"
   shows "F face_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow>
          F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<ge> b}"
@@ -650,22 +650,22 @@
   where "T exposed_face_of S \<longleftrightarrow>
          T face_of S \<and> (\<exists>a b. S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b})"
 
-lemma%unimportant empty_exposed_face_of [iff]: "{} exposed_face_of S"
+lemma empty_exposed_face_of [iff]: "{} exposed_face_of S"
   apply (simp add: exposed_face_of_def)
   apply (rule_tac x=0 in exI)
   apply (rule_tac x=1 in exI, force)
   done
 
-lemma%unimportant exposed_face_of_refl_eq [simp]: "S exposed_face_of S \<longleftrightarrow> convex S"
+lemma exposed_face_of_refl_eq [simp]: "S exposed_face_of S \<longleftrightarrow> convex S"
   apply (simp add: exposed_face_of_def face_of_refl_eq, auto)
   apply (rule_tac x=0 in exI)+
   apply force
   done
 
-lemma%unimportant exposed_face_of_refl: "convex S \<Longrightarrow> S exposed_face_of S"
+lemma exposed_face_of_refl: "convex S \<Longrightarrow> S exposed_face_of S"
   by simp
 
-lemma%unimportant exposed_face_of:
+lemma exposed_face_of:
     "T exposed_face_of S \<longleftrightarrow>
      T face_of S \<and>
      (T = {} \<or> T = S \<or>
@@ -688,19 +688,19 @@
   qed
 qed
 
-lemma%unimportant exposed_face_of_Int_supporting_hyperplane_le:
+lemma exposed_face_of_Int_supporting_hyperplane_le:
    "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
 by (force simp: exposed_face_of_def face_of_Int_supporting_hyperplane_le)
 
-lemma%unimportant exposed_face_of_Int_supporting_hyperplane_ge:
+lemma exposed_face_of_Int_supporting_hyperplane_ge:
    "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
 using exposed_face_of_Int_supporting_hyperplane_le [of S "-a" "-b"] by simp
 
-proposition%important exposed_face_of_Int:
+proposition exposed_face_of_Int:
   assumes "T exposed_face_of S"
       and "u exposed_face_of S"
     shows "(T \<inter> u) exposed_face_of S"
-proof%unimportant -
+proof -
   obtain a b where T: "S \<inter> {x. a \<bullet> x = b} face_of S"
                and S: "S \<subseteq> {x. a \<bullet> x \<le> b}"
                and teq: "T = S \<inter> {x. a \<bullet> x = b}"
@@ -722,12 +722,12 @@
     done
 qed
 
-proposition%important exposed_face_of_Inter:
+proposition exposed_face_of_Inter:
     fixes P :: "'a::euclidean_space set set"
   assumes "P \<noteq> {}"
       and "\<And>T. T \<in> P \<Longrightarrow> T exposed_face_of S"
     shows "\<Inter>P exposed_face_of S"
-proof%unimportant -
+proof -
   obtain Q where "finite Q" and QsubP: "Q \<subseteq> P" "card Q \<le> DIM('a) + 2" and IntQ: "\<Inter>Q = \<Inter>P"
     using Inter_faces_finite_altbound [of P S] assms [unfolded exposed_face_of]
     by force
@@ -749,14 +749,14 @@
   qed
 qed
 
-proposition%important exposed_face_of_sums:
+proposition exposed_face_of_sums:
   assumes "convex S" and "convex T"
       and "F exposed_face_of {x + y | x y. x \<in> S \<and> y \<in> T}"
           (is "F exposed_face_of ?ST")
   obtains k l
     where "k exposed_face_of S" "l exposed_face_of T"
           "F = {x + y | x y. x \<in> k \<and> y \<in> l}"
-proof%unimportant (cases "F = {}")
+proof (cases "F = {}")
   case True then show ?thesis
     using that by blast
 next
@@ -805,14 +805,14 @@
   qed
 qed
 
-lemma%important exposed_face_of_parallel:
+proposition exposed_face_of_parallel:
    "T exposed_face_of S \<longleftrightarrow>
          T face_of S \<and>
          (\<exists>a b. S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b} \<and>
                 (T \<noteq> {} \<longrightarrow> T \<noteq> S \<longrightarrow> a \<noteq> 0) \<and>
                 (T \<noteq> S \<longrightarrow> (\<forall>w \<in> affine hull S. (w + a) \<in> affine hull S)))"
   (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume ?lhs then show ?rhs
   proof (clarsimp simp: exposed_face_of_def)
     fix a b
@@ -881,33 +881,33 @@
   where "x extreme_point_of S \<longleftrightarrow>
          x \<in> S \<and> (\<forall>a \<in> S. \<forall>b \<in> S. x \<notin> open_segment a b)"
 
-lemma%unimportant extreme_point_of_stillconvex:
+lemma extreme_point_of_stillconvex:
    "convex S \<Longrightarrow> (x extreme_point_of S \<longleftrightarrow> x \<in> S \<and> convex(S - {x}))"
   by (fastforce simp add: convex_contains_segment extreme_point_of_def open_segment_def)
 
-lemma%unimportant face_of_singleton:
+lemma face_of_singleton:
    "{x} face_of S \<longleftrightarrow> x extreme_point_of S"
 by (fastforce simp add: extreme_point_of_def face_of_def)
 
-lemma%unimportant extreme_point_not_in_REL_INTERIOR:
+lemma extreme_point_not_in_REL_INTERIOR:
     fixes S :: "'a::real_normed_vector set"
     shows "\<lbrakk>x extreme_point_of S; S \<noteq> {x}\<rbrakk> \<Longrightarrow> x \<notin> rel_interior S"
 apply (simp add: face_of_singleton [symmetric])
 apply (blast dest: face_of_disjoint_rel_interior)
 done
 
-lemma%important extreme_point_not_in_interior:
+lemma extreme_point_not_in_interior:
     fixes S :: "'a::{real_normed_vector, perfect_space} set"
     shows "x extreme_point_of S \<Longrightarrow> x \<notin> interior S"
 apply (case_tac "S = {x}")
 apply (simp add: empty_interior_finite)
 by (meson contra_subsetD extreme_point_not_in_REL_INTERIOR interior_subset_rel_interior)
 
-lemma%unimportant extreme_point_of_face:
+lemma extreme_point_of_face:
      "F face_of S \<Longrightarrow> v extreme_point_of F \<longleftrightarrow> v extreme_point_of S \<and> v \<in> F"
   by (meson empty_subsetI face_of_face face_of_singleton insert_subset)
 
-lemma%unimportant extreme_point_of_convex_hull:
+lemma extreme_point_of_convex_hull:
    "x extreme_point_of (convex hull S) \<Longrightarrow> x \<in> S"
 apply (simp add: extreme_point_of_stillconvex)
 using hull_minimal [of S "(convex hull S) - {x}" convex]
@@ -915,58 +915,58 @@
 apply blast
 done
 
-lemma%important extreme_points_of_convex_hull:
+proposition extreme_points_of_convex_hull:
    "{x. x extreme_point_of (convex hull S)} \<subseteq> S"
-using%unimportant extreme_point_of_convex_hull by auto
-
-lemma%unimportant extreme_point_of_empty [simp]: "\<not> (x extreme_point_of {})"
+  using extreme_point_of_convex_hull by auto
+
+lemma extreme_point_of_empty [simp]: "\<not> (x extreme_point_of {})"
   by (simp add: extreme_point_of_def)
 
-lemma%unimportant extreme_point_of_singleton [iff]: "x extreme_point_of {a} \<longleftrightarrow> x = a"
+lemma extreme_point_of_singleton [iff]: "x extreme_point_of {a} \<longleftrightarrow> x = a"
   using extreme_point_of_stillconvex by auto
 
-lemma%unimportant extreme_point_of_translation_eq:
+lemma extreme_point_of_translation_eq:
    "(a + x) extreme_point_of (image (\<lambda>x. a + x) S) \<longleftrightarrow> x extreme_point_of S"
 by (auto simp: extreme_point_of_def)
 
-lemma%important extreme_points_of_translation:
+lemma extreme_points_of_translation:
    "{x. x extreme_point_of (image (\<lambda>x. a + x) S)} =
     (\<lambda>x. a + x) ` {x. x extreme_point_of S}"
-using%unimportant extreme_point_of_translation_eq
-by%unimportant auto (metis (no_types, lifting) image_iff mem_Collect_eq minus_add_cancel)
-
-lemma%important extreme_points_of_translation_subtract:
+  using extreme_point_of_translation_eq
+  by auto (metis (no_types, lifting) image_iff mem_Collect_eq minus_add_cancel)
+
+lemma extreme_points_of_translation_subtract:
    "{x. x extreme_point_of (image (\<lambda>x. x - a) S)} =
     (\<lambda>x. x - a) ` {x. x extreme_point_of S}"
-using%unimportant extreme_points_of_translation [of "- a" S]
-by%unimportant simp
-
-lemma%unimportant extreme_point_of_Int:
+  using extreme_points_of_translation [of "- a" S]
+  by simp
+
+lemma extreme_point_of_Int:
    "\<lbrakk>x extreme_point_of S; x extreme_point_of T\<rbrakk> \<Longrightarrow> x extreme_point_of (S \<inter> T)"
 by (simp add: extreme_point_of_def)
 
-lemma%important extreme_point_of_Int_supporting_hyperplane_le:
+lemma extreme_point_of_Int_supporting_hyperplane_le:
    "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> c extreme_point_of S"
 apply (simp add: face_of_singleton [symmetric])
 by (metis face_of_Int_supporting_hyperplane_le_strong convex_singleton)
 
-lemma%unimportant extreme_point_of_Int_supporting_hyperplane_ge:
+lemma extreme_point_of_Int_supporting_hyperplane_ge:
    "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> c extreme_point_of S"
 apply (simp add: face_of_singleton [symmetric])
 by (metis face_of_Int_supporting_hyperplane_ge_strong convex_singleton)
 
-lemma%unimportant exposed_point_of_Int_supporting_hyperplane_le:
+lemma exposed_point_of_Int_supporting_hyperplane_le:
    "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> {c} exposed_face_of S"
 apply (simp add: exposed_face_of_def face_of_singleton)
 apply (force simp: extreme_point_of_Int_supporting_hyperplane_le)
 done
 
-lemma%unimportant exposed_point_of_Int_supporting_hyperplane_ge:
+lemma exposed_point_of_Int_supporting_hyperplane_ge:
     "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> {c} exposed_face_of S"
 using exposed_point_of_Int_supporting_hyperplane_le [of S "-a" "-b" c]
 by simp
 
-lemma%unimportant extreme_point_of_convex_hull_insert:
+lemma extreme_point_of_convex_hull_insert:
    "\<lbrakk>finite S; a \<notin> convex hull S\<rbrakk> \<Longrightarrow> a extreme_point_of (convex hull (insert a S))"
 apply (case_tac "a \<in> S")
 apply (simp add: hull_inc)
@@ -980,34 +980,34 @@
                     (infixr "(facet'_of)" 50)
   where "F facet_of S \<longleftrightarrow> F face_of S \<and> F \<noteq> {} \<and> aff_dim F = aff_dim S - 1"
 
-lemma%unimportant facet_of_empty [simp]: "\<not> S facet_of {}"
+lemma facet_of_empty [simp]: "\<not> S facet_of {}"
   by (simp add: facet_of_def)
 
-lemma%unimportant facet_of_irrefl [simp]: "\<not> S facet_of S "
+lemma facet_of_irrefl [simp]: "\<not> S facet_of S "
   by (simp add: facet_of_def)
 
-lemma%unimportant facet_of_imp_face_of: "F facet_of S \<Longrightarrow> F face_of S"
+lemma facet_of_imp_face_of: "F facet_of S \<Longrightarrow> F face_of S"
   by (simp add: facet_of_def)
 
-lemma%unimportant facet_of_imp_subset: "F facet_of S \<Longrightarrow> F \<subseteq> S"
+lemma facet_of_imp_subset: "F facet_of S \<Longrightarrow> F \<subseteq> S"
   by (simp add: face_of_imp_subset facet_of_def)
 
-lemma%unimportant hyperplane_facet_of_halfspace_le:
+lemma hyperplane_facet_of_halfspace_le:
    "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<le> b}"
 unfolding facet_of_def hyperplane_eq_empty
 by (auto simp: hyperplane_face_of_halfspace_ge hyperplane_face_of_halfspace_le
            DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_le)
 
-lemma%unimportant hyperplane_facet_of_halfspace_ge:
+lemma hyperplane_facet_of_halfspace_ge:
     "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<ge> b}"
 unfolding facet_of_def hyperplane_eq_empty
 by (auto simp: hyperplane_face_of_halfspace_le hyperplane_face_of_halfspace_ge
            DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_ge)
 
-lemma%important facet_of_halfspace_le:
+lemma facet_of_halfspace_le:
     "F facet_of {x. a \<bullet> x \<le> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
     (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume c: ?lhs
   with c facet_of_irrefl show ?rhs
     by (force simp: aff_dim_halfspace_le facet_of_def face_of_halfspace_le cong: conj_cong split: if_split_asm)
@@ -1016,26 +1016,26 @@
     by (simp add: hyperplane_facet_of_halfspace_le)
 qed
 
-lemma%unimportant facet_of_halfspace_ge:
+lemma facet_of_halfspace_ge:
     "F facet_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
 using facet_of_halfspace_le [of F "-a" "-b"] by simp
 
-subsection \<open>Edges: faces of affine dimension 1\<close>
+subsection \<open>Edges: faces of affine dimension 1\<close> (*FIXME too small subsection, rearrange? *)
 
 definition%important edge_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"  (infixr "(edge'_of)" 50)
   where "e edge_of S \<longleftrightarrow> e face_of S \<and> aff_dim e = 1"
 
-lemma%unimportant edge_of_imp_subset:
+lemma edge_of_imp_subset:
    "S edge_of T \<Longrightarrow> S \<subseteq> T"
 by (simp add: edge_of_def face_of_imp_subset)
 
 subsection\<open>Existence of extreme points\<close>
 
-lemma%important different_norm_3_collinear_points:
+proposition different_norm_3_collinear_points:
   fixes a :: "'a::euclidean_space"
   assumes "x \<in> open_segment a b" "norm(a) = norm(b)" "norm(x) = norm(b)"
   shows False
-proof%unimportant -
+proof -
   obtain u where "norm ((1 - u) *\<^sub>R a + u *\<^sub>R b) = norm b"
              and "a \<noteq> b"
              and u01: "0 < u" "u < 1"
@@ -1056,11 +1056,11 @@
     using \<open>a \<noteq> b\<close> by force
 qed
 
-proposition%important extreme_point_exists_convex:
+proposition extreme_point_exists_convex:
   fixes S :: "'a::euclidean_space set"
   assumes "compact S" "convex S" "S \<noteq> {}"
   obtains x where "x extreme_point_of S"
-proof%unimportant -
+proof -
   obtain x where "x \<in> S" and xsup: "\<And>y. y \<in> S \<Longrightarrow> norm y \<le> norm x"
     using distance_attains_sup [of S 0] assms by auto
   have False if "a \<in> S" "b \<in> S" and x: "x \<in> open_segment a b" for a b
@@ -1107,11 +1107,11 @@
 
 subsection\<open>Krein-Milman, the weaker form\<close>
 
-proposition%important Krein_Milman:
+proposition Krein_Milman:
   fixes S :: "'a::euclidean_space set"
   assumes "compact S" "convex S"
     shows "S = closure(convex hull {x. x extreme_point_of S})"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
   case True then show ?thesis   by simp
 next
   case False
@@ -1161,12 +1161,12 @@
 
 text\<open>Now the sharper form.\<close>
 
-lemma%important Krein_Milman_Minkowski_aux:
+lemma Krein_Milman_Minkowski_aux:
   fixes S :: "'a::euclidean_space set"
   assumes n: "dim S = n" and S: "compact S" "convex S" "0 \<in> S"
     shows "0 \<in> convex hull {x. x extreme_point_of S}"
 using n S
-proof%unimportant (induction n arbitrary: S rule: less_induct)
+proof (induction n arbitrary: S rule: less_induct)
   case (less n S) show ?case
   proof (cases "0 \<in> rel_interior S")
     case True with Krein_Milman show ?thesis
@@ -1203,11 +1203,11 @@
 qed
 
 
-theorem%important Krein_Milman_Minkowski:
+theorem Krein_Milman_Minkowski:
   fixes S :: "'a::euclidean_space set"
   assumes "compact S" "convex S"
     shows "S = convex hull {x. x extreme_point_of S}"
-proof%unimportant
+proof
   show "S \<subseteq> convex hull {x. x extreme_point_of S}"
   proof
     fix a assume [simp]: "a \<in> S"
@@ -1233,15 +1233,15 @@
 
 subsection\<open>Applying it to convex hulls of explicitly indicated finite sets\<close>
 
-lemma%important Krein_Milman_polytope:
+corollary Krein_Milman_polytope:
   fixes S :: "'a::euclidean_space set"
   shows
    "finite S
        \<Longrightarrow> convex hull S =
            convex hull {x. x extreme_point_of (convex hull S)}"
-by%unimportant (simp add: Krein_Milman_Minkowski finite_imp_compact_convex_hull)
-
-lemma%unimportant extreme_points_of_convex_hull_eq:
+  by (simp add: Krein_Milman_Minkowski finite_imp_compact_convex_hull)
+
+lemma extreme_points_of_convex_hull_eq:
   fixes S :: "'a::euclidean_space set"
   shows
    "\<lbrakk>compact S; \<And>T. T \<subset> S \<Longrightarrow> convex hull T \<noteq> convex hull S\<rbrakk>
@@ -1249,18 +1249,18 @@
 by (metis (full_types) Krein_Milman_Minkowski compact_convex_hull convex_convex_hull extreme_points_of_convex_hull psubsetI)
 
 
-lemma%unimportant extreme_point_of_convex_hull_eq:
+lemma extreme_point_of_convex_hull_eq:
   fixes S :: "'a::euclidean_space set"
   shows
    "\<lbrakk>compact S; \<And>T. T \<subset> S \<Longrightarrow> convex hull T \<noteq> convex hull S\<rbrakk>
     \<Longrightarrow> (x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
 using extreme_points_of_convex_hull_eq by auto
 
-lemma%important extreme_point_of_convex_hull_convex_independent:
+lemma extreme_point_of_convex_hull_convex_independent:
   fixes S :: "'a::euclidean_space set"
   assumes "compact S" and S: "\<And>a. a \<in> S \<Longrightarrow> a \<notin> convex hull (S - {a})"
   shows "(x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
-proof%unimportant -
+proof -
   have "convex hull T \<noteq> convex hull S" if "T \<subset> S" for T
   proof -
     obtain a where  "T \<subseteq> S" "a \<in> S" "a \<notin> T" using \<open>T \<subset> S\<close> by blast
@@ -1271,7 +1271,7 @@
     by (rule extreme_point_of_convex_hull_eq [OF \<open>compact S\<close>])
 qed
 
-lemma%unimportant extreme_point_of_convex_hull_affine_independent:
+lemma extreme_point_of_convex_hull_affine_independent:
   fixes S :: "'a::euclidean_space set"
   shows
    "\<not> affine_dependent S
@@ -1279,7 +1279,7 @@
 by (metis aff_independent_finite affine_dependent_def affine_hull_convex_hull extreme_point_of_convex_hull_convex_independent finite_imp_compact hull_inc)
 
 text\<open>Elementary proofs exist, not requiring Euclidean spaces and all this development\<close>
-lemma%unimportant extreme_point_of_convex_hull_2:
+lemma extreme_point_of_convex_hull_2:
   fixes x :: "'a::euclidean_space"
   shows "x extreme_point_of (convex hull {a,b}) \<longleftrightarrow> x = a \<or> x = b"
 proof -
@@ -1289,13 +1289,13 @@
     by simp
 qed
 
-lemma%unimportant extreme_point_of_segment:
+lemma extreme_point_of_segment:
   fixes x :: "'a::euclidean_space"
   shows
    "x extreme_point_of closed_segment a b \<longleftrightarrow> x = a \<or> x = b"
 by (simp add: extreme_point_of_convex_hull_2 segment_convex_hull)
 
-lemma%unimportant face_of_convex_hull_subset:
+lemma face_of_convex_hull_subset:
   fixes S :: "'a::euclidean_space set"
   assumes "compact S" and T: "T face_of (convex hull S)"
   obtains s' where "s' \<subseteq> S" "T = convex hull s'"
@@ -1304,11 +1304,11 @@
 by (metis (no_types) Krein_Milman_Minkowski assms compact_convex_hull convex_convex_hull face_of_imp_compact face_of_imp_convex)
 
 
-lemma%important face_of_convex_hull_aux:
+lemma face_of_convex_hull_aux:
   assumes eq: "x *\<^sub>R p = u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c"
     and x: "u + v + w = x" "x \<noteq> 0" and S: "affine S" "a \<in> S" "b \<in> S" "c \<in> S"
   shows "p \<in> S"
-proof%unimportant -
+proof -
   have "p = (u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c) /\<^sub>R x"
     by (metis \<open>x \<noteq> 0\<close> eq mult.commute right_inverse scaleR_one scaleR_scaleR)
   moreover have "affine hull {a,b,c} \<subseteq> S"
@@ -1323,14 +1323,14 @@
   ultimately show ?thesis by force
 qed
 
-proposition%important face_of_convex_hull_insert_eq:
+proposition face_of_convex_hull_insert_eq:
   fixes a :: "'a :: euclidean_space"
   assumes "finite S" and a: "a \<notin> affine hull S"
   shows "(F face_of (convex hull (insert a S)) \<longleftrightarrow>
           F face_of (convex hull S) \<or>
           (\<exists>F'. F' face_of (convex hull S) \<and> F = convex hull (insert a F')))"
          (is "F face_of ?CAS \<longleftrightarrow> _")
-proof%unimportant safe
+proof safe
   assume F: "F face_of ?CAS"
     and *: "\<nexists>F'. F' face_of convex hull S \<and> F = convex hull insert a F'"
   obtain T where T: "T \<subseteq> insert a S" and FeqT: "F = convex hull T"
@@ -1471,18 +1471,18 @@
   qed
 qed
 
-lemma%unimportant face_of_convex_hull_insert2:
+lemma face_of_convex_hull_insert2:
   fixes a :: "'a :: euclidean_space"
   assumes S: "finite S" and a: "a \<notin> affine hull S" and F: "F face_of convex hull S"
   shows "convex hull (insert a F) face_of convex hull (insert a S)"
   by (metis F face_of_convex_hull_insert_eq [OF S a])
 
-proposition%important face_of_convex_hull_affine_independent:
+proposition face_of_convex_hull_affine_independent:
   fixes S :: "'a::euclidean_space set"
   assumes "\<not> affine_dependent S"
     shows "(T face_of (convex hull S) \<longleftrightarrow> (\<exists>c. c \<subseteq> S \<and> T = convex hull c))"
           (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume ?lhs
   then show ?rhs
     by (meson \<open>T face_of convex hull S\<close> aff_independent_finite assms face_of_convex_hull_subset finite_imp_compact)
@@ -1499,7 +1499,7 @@
     by (metis face_of_convex_hulls \<open>c \<subseteq> S\<close> aff_independent_finite assms T)
 qed
 
-lemma%unimportant facet_of_convex_hull_affine_independent:
+lemma facet_of_convex_hull_affine_independent:
   fixes S :: "'a::euclidean_space set"
   assumes "\<not> affine_dependent S"
     shows "T facet_of (convex hull S) \<longleftrightarrow>
@@ -1546,7 +1546,7 @@
     done
 qed
 
-lemma%unimportant facet_of_convex_hull_affine_independent_alt:
+lemma facet_of_convex_hull_affine_independent_alt:
   fixes S :: "'a::euclidean_space set"
   shows
    "\<not>affine_dependent S
@@ -1557,7 +1557,7 @@
 apply (metis Diff_cancel Int_empty_right Int_insert_right_if1  aff_independent_finite card_eq_0_iff card_insert_if card_mono card_subset_eq convex_hull_eq_empty eq_iff equals0D finite_insert finite_subset inf.absorb_iff2 insert_absorb insert_not_empty  not_less_eq_eq numeral_2_eq_2)
 done
 
-lemma%unimportant segment_face_of:
+lemma segment_face_of:
   assumes "(closed_segment a b) face_of S"
   shows "a extreme_point_of S" "b extreme_point_of S"
 proof -
@@ -1577,12 +1577,12 @@
 qed
 
 
-lemma%important Krein_Milman_frontier:
+proposition Krein_Milman_frontier:
   fixes S :: "'a::euclidean_space set"
   assumes "convex S" "compact S"
     shows "S = convex hull (frontier S)"
           (is "?lhs = ?rhs")
-proof%unimportant
+proof
   have "?lhs \<subseteq> convex hull {x. x extreme_point_of S}"
     using Krein_Milman_Minkowski assms by blast
   also have "... \<subseteq> ?rhs"
@@ -1604,31 +1604,31 @@
 definition%important polytope where
  "polytope S \<equiv> \<exists>v. finite v \<and> S = convex hull v"
 
-lemma%unimportant polytope_translation_eq: "polytope (image (\<lambda>x. a + x) S) \<longleftrightarrow> polytope S"
+lemma polytope_translation_eq: "polytope (image (\<lambda>x. a + x) S) \<longleftrightarrow> polytope S"
 apply (simp add: polytope_def, safe)
 apply (metis convex_hull_translation finite_imageI translation_galois)
 by (metis convex_hull_translation finite_imageI)
 
-lemma%unimportant polytope_linear_image: "\<lbrakk>linear f; polytope p\<rbrakk> \<Longrightarrow> polytope(image f p)"
+lemma polytope_linear_image: "\<lbrakk>linear f; polytope p\<rbrakk> \<Longrightarrow> polytope(image f p)"
   unfolding polytope_def using convex_hull_linear_image by blast
 
-lemma%unimportant polytope_empty: "polytope {}"
+lemma polytope_empty: "polytope {}"
   using convex_hull_empty polytope_def by blast
 
-lemma%unimportant polytope_convex_hull: "finite S \<Longrightarrow> polytope(convex hull S)"
+lemma polytope_convex_hull: "finite S \<Longrightarrow> polytope(convex hull S)"
   using polytope_def by auto
 
-lemma%unimportant polytope_Times: "\<lbrakk>polytope S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<times> T)"
+lemma polytope_Times: "\<lbrakk>polytope S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<times> T)"
   unfolding polytope_def
   by (metis finite_cartesian_product convex_hull_Times)
 
-lemma%unimportant face_of_polytope_polytope:
+lemma face_of_polytope_polytope:
   fixes S :: "'a::euclidean_space set"
   shows "\<lbrakk>polytope S; F face_of S\<rbrakk> \<Longrightarrow> polytope F"
 unfolding polytope_def
 by (meson face_of_convex_hull_subset finite_imp_compact finite_subset)
 
-lemma%unimportant finite_polytope_faces:
+lemma finite_polytope_faces:
   fixes S :: "'a::euclidean_space set"
   assumes "polytope S"
   shows "finite {F. F face_of S}"
@@ -1643,48 +1643,48 @@
     by (blast intro: finite_subset)
 qed
 
-lemma%unimportant finite_polytope_facets:
+lemma finite_polytope_facets:
   assumes "polytope S"
   shows "finite {T. T facet_of S}"
 by (simp add: assms facet_of_def finite_polytope_faces)
 
-lemma%unimportant polytope_scaling:
+lemma polytope_scaling:
   assumes "polytope S"  shows "polytope (image (\<lambda>x. c *\<^sub>R x) S)"
 by (simp add: assms polytope_linear_image)
 
-lemma%unimportant polytope_imp_compact:
+lemma polytope_imp_compact:
   fixes S :: "'a::real_normed_vector set"
   shows "polytope S \<Longrightarrow> compact S"
 by (metis finite_imp_compact_convex_hull polytope_def)
 
-lemma%unimportant polytope_imp_convex: "polytope S \<Longrightarrow> convex S"
+lemma polytope_imp_convex: "polytope S \<Longrightarrow> convex S"
   by (metis convex_convex_hull polytope_def)
 
-lemma%unimportant polytope_imp_closed:
+lemma polytope_imp_closed:
   fixes S :: "'a::real_normed_vector set"
   shows "polytope S \<Longrightarrow> closed S"
 by (simp add: compact_imp_closed polytope_imp_compact)
 
-lemma%unimportant polytope_imp_bounded:
+lemma polytope_imp_bounded:
   fixes S :: "'a::real_normed_vector set"
   shows "polytope S \<Longrightarrow> bounded S"
 by (simp add: compact_imp_bounded polytope_imp_compact)
 
-lemma%unimportant polytope_interval: "polytope(cbox a b)"
+lemma polytope_interval: "polytope(cbox a b)"
   unfolding polytope_def by (meson closed_interval_as_convex_hull)
 
-lemma%unimportant polytope_sing: "polytope {a}"
+lemma polytope_sing: "polytope {a}"
   using polytope_def by force
 
-lemma%unimportant face_of_polytope_insert:
+lemma face_of_polytope_insert:
      "\<lbrakk>polytope S; a \<notin> affine hull S; F face_of S\<rbrakk> \<Longrightarrow> F face_of convex hull (insert a S)"
   by (metis (no_types, lifting) affine_hull_convex_hull face_of_convex_hull_insert hull_insert polytope_def)
 
-lemma%important face_of_polytope_insert2:
+proposition face_of_polytope_insert2:
   fixes a :: "'a :: euclidean_space"
   assumes "polytope S" "a \<notin> affine hull S" "F face_of S"
   shows "convex hull (insert a F) face_of convex hull (insert a S)"
-proof%unimportant -
+proof -
   obtain V where "finite V" "S = convex hull V"
     using assms by (auto simp: polytope_def)
   then have "convex hull (insert a F) face_of convex hull (insert a V)"
@@ -1702,23 +1702,23 @@
             S = \<Inter> F \<and>
             (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b})"
 
-lemma%unimportant polyhedron_Int [intro,simp]:
+lemma polyhedron_Int [intro,simp]:
    "\<lbrakk>polyhedron S; polyhedron T\<rbrakk> \<Longrightarrow> polyhedron (S \<inter> T)"
   apply (simp add: polyhedron_def, clarify)
   apply (rename_tac F G)
   apply (rule_tac x="F \<union> G" in exI, auto)
   done
 
-lemma%unimportant polyhedron_UNIV [iff]: "polyhedron UNIV"
+lemma polyhedron_UNIV [iff]: "polyhedron UNIV"
   unfolding polyhedron_def
   by (rule_tac x="{}" in exI) auto
 
-lemma%unimportant polyhedron_Inter [intro,simp]:
+lemma polyhedron_Inter [intro,simp]:
    "\<lbrakk>finite F; \<And>S. S \<in> F \<Longrightarrow> polyhedron S\<rbrakk> \<Longrightarrow> polyhedron(\<Inter>F)"
 by (induction F rule: finite_induct) auto
 
 
-lemma%unimportant polyhedron_empty [iff]: "polyhedron ({} :: 'a :: euclidean_space set)"
+lemma polyhedron_empty [iff]: "polyhedron ({} :: 'a :: euclidean_space set)"
 proof -
   have "\<exists>a. a \<noteq> 0 \<and>
              (\<exists>b. {x. (SOME i. i \<in> Basis) \<bullet> x \<le> - 1} = {x. a \<bullet> x \<le> b})"
@@ -1737,7 +1737,7 @@
     done
 qed
 
-lemma%unimportant polyhedron_halfspace_le:
+lemma polyhedron_halfspace_le:
   fixes a :: "'a :: euclidean_space"
   shows "polyhedron {x. a \<bullet> x \<le> b}"
 proof (cases "a = 0")
@@ -1749,39 +1749,39 @@
     by (rule_tac x="{{x. a \<bullet> x \<le> b}}" in exI) auto
 qed
 
-lemma%unimportant polyhedron_halfspace_ge:
+lemma polyhedron_halfspace_ge:
   fixes a :: "'a :: euclidean_space"
   shows "polyhedron {x. a \<bullet> x \<ge> b}"
 using polyhedron_halfspace_le [of "-a" "-b"] by simp
 
-lemma%important polyhedron_hyperplane:
+lemma polyhedron_hyperplane:
   fixes a :: "'a :: euclidean_space"
   shows "polyhedron {x. a \<bullet> x = b}"
-proof%unimportant -
+proof -
   have "{x. a \<bullet> x = b} = {x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x \<ge> b}"
     by force
   then show ?thesis
     by (simp add: polyhedron_halfspace_ge polyhedron_halfspace_le)
 qed
 
-lemma%unimportant affine_imp_polyhedron:
+lemma affine_imp_polyhedron:
   fixes S :: "'a :: euclidean_space set"
   shows "affine S \<Longrightarrow> polyhedron S"
 by (metis affine_hull_eq polyhedron_Inter polyhedron_hyperplane affine_hull_finite_intersection_hyperplanes [of S])
 
-lemma%unimportant polyhedron_imp_closed:
+lemma polyhedron_imp_closed:
   fixes S :: "'a :: euclidean_space set"
   shows "polyhedron S \<Longrightarrow> closed S"
 apply (simp add: polyhedron_def)
 using closed_halfspace_le by fastforce
 
-lemma%unimportant polyhedron_imp_convex:
+lemma polyhedron_imp_convex:
   fixes S :: "'a :: euclidean_space set"
   shows "polyhedron S \<Longrightarrow> convex S"
 apply (simp add: polyhedron_def)
 using convex_Inter convex_halfspace_le by fastforce
 
-lemma%unimportant polyhedron_affine_hull:
+lemma polyhedron_affine_hull:
   fixes S :: "'a :: euclidean_space set"
   shows "polyhedron(affine hull S)"
 by (simp add: affine_imp_polyhedron)
@@ -1789,13 +1789,13 @@
 
 subsection\<open>Canonical polyhedron representation making facial structure explicit\<close>
 
-lemma%important polyhedron_Int_affine:
+proposition polyhedron_Int_affine:
   fixes S :: "'a :: euclidean_space set"
   shows "polyhedron S \<longleftrightarrow>
            (\<exists>F. finite F \<and> S = (affine hull S) \<inter> \<Inter>F \<and>
                 (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}))"
         (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume ?lhs then show ?rhs
     apply (simp add: polyhedron_def)
     apply (erule ex_forward)
@@ -1809,13 +1809,13 @@
     done
 qed
 
-proposition%important rel_interior_polyhedron_explicit:
+proposition rel_interior_polyhedron_explicit:
   assumes "finite F"
       and seq: "S = affine hull S \<inter> \<Inter>F"
       and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
       and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
     shows "rel_interior S = {x \<in> S. \<forall>h \<in> F. a h \<bullet> x < b h}"
-proof%unimportant -
+proof -
   have rels: "\<And>x. x \<in> rel_interior S \<Longrightarrow> x \<in> S"
     by (meson IntE mem_rel_interior)
   moreover have "a i \<bullet> x < b i" if x: "x \<in> rel_interior S" and "i \<in> F" for x i
@@ -1883,7 +1883,7 @@
 qed
 
 
-lemma%important polyhedron_Int_affine_parallel:
+lemma polyhedron_Int_affine_parallel:
   fixes S :: "'a :: euclidean_space set"
   shows "polyhedron S \<longleftrightarrow>
          (\<exists>F. finite F \<and>
@@ -1891,7 +1891,7 @@
               (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b} \<and>
                              (\<forall>x \<in> affine hull S. (x + a) \<in> affine hull S)))"
     (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume ?lhs
   then obtain F where "finite F" and seq: "S = (affine hull S) \<inter> \<Inter>F"
                   and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
@@ -1937,7 +1937,7 @@
 qed
 
 
-proposition%important polyhedron_Int_affine_parallel_minimal:
+proposition polyhedron_Int_affine_parallel_minimal:
   fixes S :: "'a :: euclidean_space set"
   shows "polyhedron S \<longleftrightarrow>
          (\<exists>F. finite F \<and>
@@ -1946,7 +1946,7 @@
                              (\<forall>x \<in> affine hull S. (x + a) \<in> affine hull S)) \<and>
               (\<forall>F'. F' \<subset> F \<longrightarrow> S \<subset> (affine hull S) \<inter> (\<Inter>F')))"
     (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume ?lhs
   then obtain f0
            where f0: "finite f0"
@@ -1982,7 +1982,7 @@
 qed
 
 
-lemma%unimportant polyhedron_Int_affine_minimal:
+lemma polyhedron_Int_affine_minimal:
   fixes S :: "'a :: euclidean_space set"
   shows "polyhedron S \<longleftrightarrow>
          (\<exists>F. finite F \<and> S = (affine hull S) \<inter> \<Inter>F \<and>
@@ -1993,13 +1993,13 @@
 apply (auto simp: polyhedron_Int_affine elim!: ex_forward)
 done
 
-proposition%important facet_of_polyhedron_explicit:
+proposition facet_of_polyhedron_explicit:
   assumes "finite F"
       and seq: "S = affine hull S \<inter> \<Inter>F"
       and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
       and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
     shows "c facet_of S \<longleftrightarrow> (\<exists>h. h \<in> F \<and> c = S \<inter> {x. a h \<bullet> x = b h})"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
   case True with psub show ?thesis by force
 next
   case False
@@ -2212,7 +2212,7 @@
 qed
 
 
-lemma%important face_of_polyhedron_subset_explicit:
+lemma face_of_polyhedron_subset_explicit:
   fixes S :: "'a :: euclidean_space set"
   assumes "finite F"
       and seq: "S = affine hull S \<inter> \<Inter>F"
@@ -2220,7 +2220,7 @@
       and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
       and c: "c face_of S" and "c \<noteq> {}" "c \<noteq> S"
    obtains h where "h \<in> F" "c \<subseteq> S \<inter> {x. a h \<bullet> x = b h}"
-proof%unimportant -
+proof -
   have "c \<subseteq> S" using \<open>c face_of S\<close>
     by (simp add: face_of_imp_subset)
   have "polyhedron S"
@@ -2259,7 +2259,7 @@
 qed
 
 text\<open>Initial part of proof duplicates that above\<close>
-proposition%important face_of_polyhedron_explicit:
+proposition face_of_polyhedron_explicit:
   fixes S :: "'a :: euclidean_space set"
   assumes "finite F"
       and seq: "S = affine hull S \<inter> \<Inter>F"
@@ -2267,7 +2267,7 @@
       and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
       and c: "c face_of S" and "c \<noteq> {}" "c \<noteq> S"
     shows "c = \<Inter>{S \<inter> {x. a h \<bullet> x = b h} | h. h \<in> F \<and> c \<subseteq> S \<inter> {x. a h \<bullet> x = b h}}"
-proof%unimportant -
+proof -
   let ?ab = "\<lambda>h. {x. a h \<bullet> x = b h}"
   have "c \<subseteq> S" using \<open>c face_of S\<close>
     by (simp add: face_of_imp_subset)
@@ -2373,10 +2373,10 @@
 
 subsection\<open>More general corollaries from the explicit representation\<close>
 
-corollary%important facet_of_polyhedron:
+corollary facet_of_polyhedron:
   assumes "polyhedron S" and "c facet_of S"
   obtains a b where "a \<noteq> 0" "S \<subseteq> {x. a \<bullet> x \<le> b}" "c = S \<inter> {x. a \<bullet> x = b}"
-proof%unimportant -
+proof -
   obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
              and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
              and min: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
@@ -2393,10 +2393,10 @@
     by (rule_tac a = "a i" and b = "b i" in that) (simp_all add: ab)
 qed
 
-corollary%important face_of_polyhedron:
+corollary face_of_polyhedron:
   assumes "polyhedron S" and "c face_of S" and "c \<noteq> {}" and "c \<noteq> S"
     shows "c = \<Inter>{F. F facet_of S \<and> c \<subseteq> F}"
-proof%unimportant -
+proof -
   obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
              and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
              and min: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
@@ -2409,14 +2409,14 @@
     done
 qed
 
-lemma%unimportant face_of_polyhedron_subset_facet:
+lemma face_of_polyhedron_subset_facet:
   assumes "polyhedron S" and "c face_of S" and "c \<noteq> {}" and "c \<noteq> S"
   obtains F where "F facet_of S" "c \<subseteq> F"
 using face_of_polyhedron assms
 by (metis (no_types, lifting) Inf_greatest antisym_conv face_of_imp_subset mem_Collect_eq)
 
 
-lemma%unimportant exposed_face_of_polyhedron:
+lemma exposed_face_of_polyhedron:
   assumes "polyhedron S"
     shows "F exposed_face_of S \<longleftrightarrow> F face_of S"
 proof
@@ -2444,12 +2444,12 @@
   qed
 qed
 
-lemma%unimportant face_of_polyhedron_polyhedron:
+lemma face_of_polyhedron_polyhedron:
   fixes S :: "'a :: euclidean_space set"
   assumes "polyhedron S" "c face_of S" shows "polyhedron c"
 by (metis assms face_of_imp_eq_affine_Int polyhedron_Int polyhedron_affine_hull polyhedron_imp_convex)
 
-lemma%unimportant finite_polyhedron_faces:
+lemma finite_polyhedron_faces:
   fixes S :: "'a :: euclidean_space set"
   assumes "polyhedron S"
     shows "finite {F. F face_of S}"
@@ -2473,29 +2473,29 @@
     by (meson finite.emptyI finite.insertI finite_Diff2 finite_subset)
 qed
 
-lemma%unimportant finite_polyhedron_exposed_faces:
+lemma finite_polyhedron_exposed_faces:
    "polyhedron S \<Longrightarrow> finite {F. F exposed_face_of S}"
 using exposed_face_of_polyhedron finite_polyhedron_faces by fastforce
 
-lemma%unimportant finite_polyhedron_extreme_points:
+lemma finite_polyhedron_extreme_points:
   fixes S :: "'a :: euclidean_space set"
   shows "polyhedron S \<Longrightarrow> finite {v. v extreme_point_of S}"
 apply (simp add: face_of_singleton [symmetric])
 apply (rule finite_subset [OF _ finite_vimageI [OF finite_polyhedron_faces]], auto)
 done
 
-lemma%unimportant finite_polyhedron_facets:
+lemma finite_polyhedron_facets:
   fixes S :: "'a :: euclidean_space set"
   shows "polyhedron S \<Longrightarrow> finite {F. F facet_of S}"
 unfolding facet_of_def
 by (blast intro: finite_subset [OF _ finite_polyhedron_faces])
 
 
-proposition%important rel_interior_of_polyhedron:
+proposition rel_interior_of_polyhedron:
   fixes S :: "'a :: euclidean_space set"
   assumes "polyhedron S"
     shows "rel_interior S = S - \<Union>{F. F facet_of S}"
-proof%unimportant -
+proof -
   obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
              and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
              and min: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
@@ -2535,19 +2535,19 @@
     by (force simp: rel)
 qed
 
-lemma%unimportant rel_boundary_of_polyhedron:
+lemma rel_boundary_of_polyhedron:
   fixes S :: "'a :: euclidean_space set"
   assumes "polyhedron S"
     shows "S - rel_interior S = \<Union> {F. F facet_of S}"
 using facet_of_imp_subset by (fastforce simp add: rel_interior_of_polyhedron assms)
 
-lemma%unimportant rel_frontier_of_polyhedron:
+lemma rel_frontier_of_polyhedron:
   fixes S :: "'a :: euclidean_space set"
   assumes "polyhedron S"
     shows "rel_frontier S = \<Union> {F. F facet_of S}"
 by (simp add: assms rel_frontier_def polyhedron_imp_closed rel_boundary_of_polyhedron)
 
-lemma%unimportant rel_frontier_of_polyhedron_alt:
+lemma rel_frontier_of_polyhedron_alt:
   fixes S :: "'a :: euclidean_space set"
   assumes "polyhedron S"
     shows "rel_frontier S = \<Union> {F. F face_of S \<and> (F \<noteq> S)}"
@@ -2558,11 +2558,11 @@
 
 text\<open>A characterization of polyhedra as having finitely many faces\<close>
 
-proposition%important polyhedron_eq_finite_exposed_faces:
+proposition polyhedron_eq_finite_exposed_faces:
   fixes S :: "'a :: euclidean_space set"
   shows "polyhedron S \<longleftrightarrow> closed S \<and> convex S \<and> finite {F. F exposed_face_of S}"
          (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume ?lhs
   then show ?rhs
     by (auto simp: polyhedron_imp_closed polyhedron_imp_convex finite_polyhedron_exposed_faces)
@@ -2649,11 +2649,11 @@
   qed
 qed
 
-corollary%important polyhedron_eq_finite_faces:
+corollary polyhedron_eq_finite_faces:
   fixes S :: "'a :: euclidean_space set"
   shows "polyhedron S \<longleftrightarrow> closed S \<and> convex S \<and> finite {F. F face_of S}"
          (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume ?lhs
   then show ?rhs
     by (simp add: finite_polyhedron_faces polyhedron_imp_closed polyhedron_imp_convex)
@@ -2663,7 +2663,7 @@
     by (force simp: polyhedron_eq_finite_exposed_faces exposed_face_of intro: finite_subset)
 qed
 
-lemma%unimportant polyhedron_linear_image_eq:
+lemma polyhedron_linear_image_eq:
   fixes h :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
   assumes "linear h" "bij h"
     shows "polyhedron (h ` S) \<longleftrightarrow> polyhedron S"
@@ -2683,7 +2683,7 @@
     done
 qed
 
-lemma%unimportant polyhedron_negations:
+lemma polyhedron_negations:
   fixes S :: "'a :: euclidean_space set"
   shows   "polyhedron S \<Longrightarrow> polyhedron(image uminus S)"
   by (subst polyhedron_linear_image_eq)
@@ -2691,11 +2691,11 @@
 
 subsection\<open>Relation between polytopes and polyhedra\<close>
 
-lemma%important polytope_eq_bounded_polyhedron:
+proposition polytope_eq_bounded_polyhedron:
   fixes S :: "'a :: euclidean_space set"
   shows "polytope S \<longleftrightarrow> polyhedron S \<and> bounded S"
          (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume ?lhs
   then show ?rhs
     by (simp add: finite_polytope_faces polyhedron_eq_finite_faces
@@ -2708,28 +2708,28 @@
     done
 qed
 
-lemma%unimportant polytope_Int:
+lemma polytope_Int:
   fixes S :: "'a :: euclidean_space set"
   shows "\<lbrakk>polytope S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<inter> T)"
 by (simp add: polytope_eq_bounded_polyhedron bounded_Int)
 
 
-lemma%important polytope_Int_polyhedron:
+lemma polytope_Int_polyhedron:
   fixes S :: "'a :: euclidean_space set"
   shows "\<lbrakk>polytope S; polyhedron T\<rbrakk> \<Longrightarrow> polytope(S \<inter> T)"
-by%unimportant (simp add: bounded_Int polytope_eq_bounded_polyhedron)
-
-lemma%important polyhedron_Int_polytope:
+  by (simp add: bounded_Int polytope_eq_bounded_polyhedron)
+
+lemma polyhedron_Int_polytope:
   fixes S :: "'a :: euclidean_space set"
   shows "\<lbrakk>polyhedron S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<inter> T)"
-by%unimportant (simp add: bounded_Int polytope_eq_bounded_polyhedron)
-
-lemma%important polytope_imp_polyhedron:
+  by (simp add: bounded_Int polytope_eq_bounded_polyhedron)
+
+lemma polytope_imp_polyhedron:
   fixes S :: "'a :: euclidean_space set"
   shows "polytope S \<Longrightarrow> polyhedron S"
-by%unimportant (simp add: polytope_eq_bounded_polyhedron)
-
-lemma%unimportant polytope_facet_exists:
+  by (simp add: polytope_eq_bounded_polyhedron)
+
+lemma polytope_facet_exists:
   fixes p :: "'a :: euclidean_space set"
   assumes "polytope p" "0 < aff_dim p"
   obtains F where "F facet_of p"
@@ -2746,10 +2746,10 @@
        all_not_in_conv assms face_of_singleton less_irrefl singletonI that)
 qed
 
-lemma%unimportant polyhedron_interval [iff]: "polyhedron(cbox a b)"
+lemma polyhedron_interval [iff]: "polyhedron(cbox a b)"
 by (metis polytope_imp_polyhedron polytope_interval)
 
-lemma%unimportant polyhedron_convex_hull:
+lemma polyhedron_convex_hull:
   fixes S :: "'a :: euclidean_space set"
   shows "finite S \<Longrightarrow> polyhedron(convex hull S)"
 by (simp add: polytope_convex_hull polytope_imp_polyhedron)
@@ -3087,7 +3087,8 @@
 subsection\<open>Simplexes\<close>
 
 text\<open>The notion of n-simplex for integer \<^term>\<open>n \<ge> -1\<close>\<close>
-definition simplex :: "int \<Rightarrow> 'a::euclidean_space set \<Rightarrow> bool" (infix "simplex" 50)
+
+definition%important simplex :: "int \<Rightarrow> 'a::euclidean_space set \<Rightarrow> bool" (infix "simplex" 50)
   where "n simplex S \<equiv> \<exists>C. \<not> affine_dependent C \<and> int(card C) = n + 1 \<and> S = convex hull C"
 
 lemma simplex:
@@ -3228,7 +3229,7 @@
 
 subsection\<open>Refining a cell complex to a simplicial complex\<close>
 
-lemma%important convex_hull_insert_Int_eq:
+proposition convex_hull_insert_Int_eq:
   fixes z :: "'a :: euclidean_space"
   assumes z: "z \<in> rel_interior S"
       and T: "T \<subseteq> rel_frontier S"
@@ -3236,7 +3237,7 @@
       and "convex S" "convex T" "convex U"
   shows "convex hull (insert z T) \<inter> convex hull (insert z U) = convex hull (insert z (T \<inter> U))"
     (is "?lhs = ?rhs")
-proof%unimportant
+proof
   show "?lhs \<subseteq> ?rhs"
   proof (cases "T={} \<or> U={}")
     case True then show ?thesis by auto
@@ -3308,7 +3309,7 @@
     by (metis inf_greatest hull_mono inf.cobounded1 inf.cobounded2 insert_mono)
 qed
 
-lemma%important simplicial_subdivision_aux:
+lemma simplicial_subdivision_aux:
   assumes "finite \<M>"
       and "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
       and "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> of_nat n"
@@ -3320,7 +3321,7 @@
                 (\<forall>C \<in> \<M>. \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F) \<and>
                 (\<forall>K \<in> \<T>. \<exists>C. C \<in> \<M> \<and> K \<subseteq> C)"
   using assms
-proof%unimportant (induction n arbitrary: \<M> rule: less_induct)
+proof (induction n arbitrary: \<M> rule: less_induct)
   case (less n)
   then have poly\<M>: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
       and aff\<M>:    "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> of_nat n"
@@ -3770,7 +3771,7 @@
 qed
 
 
-lemma%important simplicial_subdivision_of_cell_complex_lowdim:
+lemma simplicial_subdivision_of_cell_complex_lowdim:
   assumes "finite \<M>"
       and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
       and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
@@ -3779,7 +3780,7 @@
                   "\<Union>\<T> = \<Union>\<M>"
                   "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
                   "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
-proof%unimportant (cases "d \<ge> 0")
+proof (cases "d \<ge> 0")
   case True
   then obtain n where n: "d = of_nat n"
     using zero_le_imp_eq_int by blast
@@ -3836,7 +3837,7 @@
   qed auto
 qed
 
-proposition%important simplicial_subdivision_of_cell_complex:
+proposition simplicial_subdivision_of_cell_complex:
   assumes "finite \<M>"
       and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
       and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
@@ -3844,9 +3845,9 @@
                   "\<Union>\<T> = \<Union>\<M>"
                   "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
                   "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
-  by%unimportant (blast intro: simplicial_subdivision_of_cell_complex_lowdim [OF assms aff_dim_le_DIM])
-
-corollary%important fine_simplicial_subdivision_of_cell_complex:
+  by (blast intro: simplicial_subdivision_of_cell_complex_lowdim [OF assms aff_dim_le_DIM])
+
+corollary fine_simplicial_subdivision_of_cell_complex:
   assumes "0 < e" "finite \<M>"
       and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
       and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
@@ -3855,7 +3856,7 @@
                   "\<Union>\<T> = \<Union>\<M>"
                   "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
                   "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
-proof%unimportant -
+proof -
   obtain \<N> where \<N>: "finite \<N>" "\<Union>\<N> = \<Union>\<M>" 
               and diapoly: "\<And>X. X \<in> \<N> \<Longrightarrow> diameter X < e" "\<And>X. X \<in> \<N> \<Longrightarrow> polytope X"
                and      "\<And>X Y. \<lbrakk>X \<in> \<N>; Y \<in> \<N>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
@@ -3896,11 +3897,11 @@
 
 subsection\<open>Some results on cell division with full-dimensional cells only\<close>
 
-lemma%important convex_Union_fulldim_cells:
+lemma convex_Union_fulldim_cells:
   assumes "finite \<S>" and clo: "\<And>C. C \<in> \<S> \<Longrightarrow> closed C" and con: "\<And>C. C \<in> \<S> \<Longrightarrow> convex C"
       and eq: "\<Union>\<S> = U"and  "convex U"
  shows "\<Union>{C \<in> \<S>. aff_dim C = aff_dim U} = U"  (is "?lhs = U")
-proof%unimportant -
+proof -
   have "closed U"
     using \<open>finite \<S>\<close> clo eq by blast
   have "?lhs \<subseteq> U"
@@ -3949,7 +3950,7 @@
   ultimately show ?thesis by blast
 qed
 
-proposition%important fine_triangular_subdivision_of_cell_complex:
+proposition fine_triangular_subdivision_of_cell_complex:
   assumes "0 < e" "finite \<M>"
       and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
       and aff: "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C = d"
@@ -3958,7 +3959,7 @@
                  "\<And>k. k \<in> \<T> \<Longrightarrow> aff_dim k = d" "\<Union>\<T> = \<Union>\<M>"
                  "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>f. finite f \<and> f \<subseteq> \<T> \<and> C = \<Union>f"
                  "\<And>k. k \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> k \<subseteq> C"
-proof%unimportant -
+proof -
   obtain \<T> where "simplicial_complex \<T>"
              and dia\<T>: "\<And>K. K \<in> \<T> \<Longrightarrow> diameter K < e"
              and "\<Union>\<T> = \<Union>\<M>"
diff -r 2444c8b85aac -r 0c3dcb3a17f6 src/HOL/Analysis/Radon_Nikodym.thy
--- a/src/HOL/Analysis/Radon_Nikodym.thy	Wed Jan 23 17:20:35 2019 +0100
+++ b/src/HOL/Analysis/Radon_Nikodym.thy	Thu Jan 24 00:28:29 2019 +0000
@@ -2,7 +2,7 @@
     Author:     Johannes Hölzl, TU München
 *)
 
-section%important \<open>Radon-Nikod{\'y}m Derivative\<close>
+section \<open>Radon-Nikod{\'y}m Derivative\<close>
 
 theory Radon_Nikodym
 imports Bochner_Integration
@@ -17,12 +17,12 @@
     and sets_diff_measure[simp]: "sets (diff_measure M N) = sets M"
   by (auto simp: diff_measure_def)
 
-lemma%important emeasure_diff_measure:
+lemma emeasure_diff_measure:
   assumes fin: "finite_measure M" "finite_measure N" and sets_eq: "sets M = sets N"
   assumes pos: "\<And>A. A \<in> sets M \<Longrightarrow> emeasure N A \<le> emeasure M A" and A: "A \<in> sets M"
   shows "emeasure (diff_measure M N) A = emeasure M A - emeasure N A" (is "_ = ?\<mu> A")
-  unfolding%unimportant diff_measure_def
-proof%unimportant (rule emeasure_measure_of_sigma)
+  unfolding diff_measure_def
+proof (rule emeasure_measure_of_sigma)
   show "sigma_algebra (space M) (sets M)" ..
   show "positive (sets M) ?\<mu>"
     using pos by (simp add: positive_def)
@@ -48,7 +48,7 @@
 positive functions (or, still equivalently, the existence of a probability measure which is in
 the same measure class as the original measure).\<close>
 
-lemma (in sigma_finite_measure) obtain_positive_integrable_function:
+proposition (in sigma_finite_measure) obtain_positive_integrable_function:
   obtains f::"'a \<Rightarrow> real" where
     "f \<in> borel_measurable M"
     "\<And>x. f x > 0"
@@ -102,9 +102,9 @@
     by (meson that)
 qed
 
-lemma%important (in sigma_finite_measure) Ex_finite_integrable_function:
+lemma (in sigma_finite_measure) Ex_finite_integrable_function:
   "\<exists>h\<in>borel_measurable M. integral\<^sup>N M h \<noteq> \<infinity> \<and> (\<forall>x\<in>space M. 0 < h x \<and> h x < \<infinity>)"
-proof%unimportant -
+proof -
   obtain A :: "nat \<Rightarrow> 'a set" where
     range[measurable]: "range A \<subseteq> sets M" and
     space: "(\<Union>i. A i) = space M" and
@@ -183,11 +183,11 @@
   "absolutely_continuous M N \<Longrightarrow> A \<in> sets M \<Longrightarrow> emeasure M A = 0 \<Longrightarrow> emeasure N A = 0"
   by (auto simp: absolutely_continuous_def null_sets_def)
 
-lemma%important absolutely_continuous_AE:
+lemma absolutely_continuous_AE:
   assumes sets_eq: "sets M' = sets M"
     and "absolutely_continuous M M'" "AE x in M. P x"
    shows "AE x in M'. P x"
-proof%unimportant -
+proof -
   from \<open>AE x in M. P x\<close> obtain N where N: "N \<in> null_sets M" "{x\<in>space M. \<not> P x} \<subseteq> N"
     unfolding eventually_ae_filter by auto
   show "AE x in M'. P x"
@@ -200,12 +200,12 @@
 
 subsection "Existence of the Radon-Nikodym derivative"
 
-lemma%important
+proposition
  (in finite_measure) Radon_Nikodym_finite_measure:
   assumes "finite_measure N" and sets_eq[simp]: "sets N = sets M"
   assumes "absolutely_continuous M N"
   shows "\<exists>f \<in> borel_measurable M. density M f = N"
-proof%unimportant -
+proof -
   interpret N: finite_measure N by fact
   define G where "G = {g \<in> borel_measurable M. \<forall>A\<in>sets M. (\<integral>\<^sup>+x. g x * indicator A x \<partial>M) \<le> N A}"
   have [measurable_dest]: "f \<in> G \<Longrightarrow> f \<in> borel_measurable M"
@@ -384,11 +384,11 @@
   qed auto
 qed
 
-lemma%important (in finite_measure) split_space_into_finite_sets_and_rest:
+lemma (in finite_measure) split_space_into_finite_sets_and_rest:
   assumes ac: "absolutely_continuous M N" and sets_eq[simp]: "sets N = sets M"
   shows "\<exists>B::nat\<Rightarrow>'a set. disjoint_family B \<and> range B \<subseteq> sets M \<and> (\<forall>i. N (B i) \<noteq> \<infinity>) \<and>
     (\<forall>A\<in>sets M. A \<inter> (\<Union>i. B i) = {} \<longrightarrow> (emeasure M A = 0 \<and> N A = 0) \<or> (emeasure M A > 0 \<and> N A = \<infinity>))"
-proof%unimportant -
+proof -
   let ?Q = "{Q\<in>sets M. N Q \<noteq> \<infinity>}"
   let ?a = "SUP Q\<in>?Q. emeasure M Q"
   have "{} \<in> ?Q" by auto
@@ -493,10 +493,10 @@
   qed
 qed
 
-lemma%important (in finite_measure) Radon_Nikodym_finite_measure_infinite:
+proposition (in finite_measure) Radon_Nikodym_finite_measure_infinite:
   assumes "absolutely_continuous M N" and sets_eq: "sets N = sets M"
   shows "\<exists>f\<in>borel_measurable M. density M f = N"
-proof%unimportant -
+proof -
   from split_space_into_finite_sets_and_rest[OF assms]
   obtain Q :: "nat \<Rightarrow> 'a set"
     where Q: "disjoint_family Q" "range Q \<subseteq> sets M"
@@ -575,7 +575,7 @@
   qed
 qed
 
-lemma (in sigma_finite_measure) Radon_Nikodym:
+theorem (in sigma_finite_measure) Radon_Nikodym:
   assumes ac: "absolutely_continuous M N" assumes sets_eq: "sets N = sets M"
   shows "\<exists>f \<in> borel_measurable M. density M f = N"
 proof -
@@ -609,12 +609,12 @@
 
 subsection \<open>Uniqueness of densities\<close>
 
-lemma%important finite_density_unique:
+lemma finite_density_unique:
   assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   assumes pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
   and fin: "integral\<^sup>N M f \<noteq> \<infinity>"
   shows "density M f = density M g \<longleftrightarrow> (AE x in M. f x = g x)"
-proof%unimportant (intro iffI ballI)
+proof (intro iffI ballI)
   fix A assume eq: "AE x in M. f x = g x"
   with borel show "density M f = density M g"
     by (auto intro: density_cong)
@@ -652,13 +652,13 @@
   show "AE x in M. f x = g x" by auto
 qed
 
-lemma%important (in finite_measure) density_unique_finite_measure:
+lemma (in finite_measure) density_unique_finite_measure:
   assumes borel: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
   assumes pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> f' x"
   assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+x. f x * indicator A x \<partial>M) = (\<integral>\<^sup>+x. f' x * indicator A x \<partial>M)"
     (is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
   shows "AE x in M. f x = f' x"
-proof%unimportant -
+proof -
   let ?D = "\<lambda>f. density M f"
   let ?N = "\<lambda>A. ?P f A" and ?N' = "\<lambda>A. ?P f' A"
   let ?f = "\<lambda>A x. f x * indicator A x" and ?f' = "\<lambda>A x. f' x * indicator A x"
@@ -717,7 +717,7 @@
   then show "AE x in M. f x = f' x" by auto
 qed
 
-lemma (in sigma_finite_measure) density_unique:
+proposition (in sigma_finite_measure) density_unique:
   assumes f: "f \<in> borel_measurable M"
   assumes f': "f' \<in> borel_measurable M"
   assumes density_eq: "density M f = density M f'"
@@ -764,11 +764,11 @@
   shows "density M f = density M f' \<longleftrightarrow> (AE x in M. f x = f' x)"
   using density_unique[OF assms] density_cong[OF f f'] by auto
 
-lemma%important sigma_finite_density_unique:
+lemma sigma_finite_density_unique:
   assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   and fin: "sigma_finite_measure (density M f)"
   shows "density M f = density M g \<longleftrightarrow> (AE x in M. f x = g x)"
-proof%unimportant
+proof
   assume "AE x in M. f x = g x" with borel show "density M f = density M g"
     by (auto intro: density_cong)
 next
@@ -797,11 +797,11 @@
     done
 qed
 
-lemma%important (in sigma_finite_measure) sigma_finite_iff_density_finite':
+lemma (in sigma_finite_measure) sigma_finite_iff_density_finite':
   assumes f: "f \<in> borel_measurable M"
   shows "sigma_finite_measure (density M f) \<longleftrightarrow> (AE x in M. f x \<noteq> \<infinity>)"
     (is "sigma_finite_measure ?N \<longleftrightarrow> _")
-proof%unimportant
+proof
   assume "sigma_finite_measure ?N"
   then interpret N: sigma_finite_measure ?N .
   from N.Ex_finite_integrable_function obtain h where
@@ -895,10 +895,10 @@
        then SOME f. f \<in> borel_measurable M \<and> density M f = N
        else (\<lambda>_. 0))"
 
-lemma%important RN_derivI:
+lemma RN_derivI:
   assumes "f \<in> borel_measurable M" "density M f = N"
   shows "density M (RN_deriv M N) = N"
-proof%unimportant -
+proof -
   have *: "\<exists>f. f \<in> borel_measurable M \<and> density M f = N"
     using assms by auto
   then have "density M (SOME f. f \<in> borel_measurable M \<and> density M f = N) = N"
@@ -925,11 +925,11 @@
   "absolutely_continuous M N \<Longrightarrow> sets N = sets M \<Longrightarrow> density M (RN_deriv M N) = N"
   by (metis RN_derivI Radon_Nikodym)
 
-lemma%important (in sigma_finite_measure) RN_deriv_nn_integral:
+lemma (in sigma_finite_measure) RN_deriv_nn_integral:
   assumes N: "absolutely_continuous M N" "sets N = sets M"
     and f: "f \<in> borel_measurable M"
   shows "integral\<^sup>N N f = (\<integral>\<^sup>+x. RN_deriv M N x * f x \<partial>M)"
-proof%unimportant -
+proof -
   have "integral\<^sup>N N f = integral\<^sup>N (density M (RN_deriv M N)) f"
     using N by (simp add: density_RN_deriv)
   also have "\<dots> = (\<integral>\<^sup>+x. RN_deriv M N x * f x \<partial>M)"
@@ -953,14 +953,14 @@
   by (intro sigma_finite_density_unique[THEN iffD1] f borel_measurable_RN_deriv
             density_RN_deriv_density[symmetric])
 
-lemma%important (in sigma_finite_measure) RN_deriv_distr:
+lemma (in sigma_finite_measure) RN_deriv_distr:
   fixes T :: "'a \<Rightarrow> 'b"
   assumes T: "T \<in> measurable M M'" and T': "T' \<in> measurable M' M"
     and inv: "\<forall>x\<in>space M. T' (T x) = x"
   and ac[simp]: "absolutely_continuous (distr M M' T) (distr N M' T)"
   and N: "sets N = sets M"
   shows "AE x in M. RN_deriv (distr M M' T) (distr N M' T) (T x) = RN_deriv M N x"
-proof%unimportant (rule RN_deriv_unique)
+proof (rule RN_deriv_unique)
   have [simp]: "sets N = sets M" by fact
   note sets_eq_imp_space_eq[OF N, simp]
   have measurable_N[simp]: "\<And>M'. measurable N M' = measurable M M'" by (auto simp: measurable_def)
@@ -1012,23 +1012,23 @@
     by (simp add: comp_def)
 qed
 
-lemma%important (in sigma_finite_measure) RN_deriv_finite:
+lemma (in sigma_finite_measure) RN_deriv_finite:
   assumes N: "sigma_finite_measure N" and ac: "absolutely_continuous M N" "sets N = sets M"
   shows "AE x in M. RN_deriv M N x \<noteq> \<infinity>"
-proof%unimportant -
+proof -
   interpret N: sigma_finite_measure N by fact
   from N show ?thesis
     using sigma_finite_iff_density_finite[OF borel_measurable_RN_deriv, of N] density_RN_deriv[OF ac]
     by simp
 qed
 
-lemma%important (in sigma_finite_measure) (* *FIX ME needs name*)
+lemma (in sigma_finite_measure) (* FIXME needs name*)
   assumes N: "sigma_finite_measure N" and ac: "absolutely_continuous M N" "sets N = sets M"
     and f: "f \<in> borel_measurable M"
   shows RN_deriv_integrable: "integrable N f \<longleftrightarrow>
       integrable M (\<lambda>x. enn2real (RN_deriv M N x) * f x)" (is ?integrable)
     and RN_deriv_integral: "integral\<^sup>L N f = (\<integral>x. enn2real (RN_deriv M N x) * f x \<partial>M)" (is ?integral)
-proof%unimportant -
+proof -
   note ac(2)[simp] and sets_eq_imp_space_eq[OF ac(2), simp]
   interpret N: sigma_finite_measure N by fact
 
@@ -1054,14 +1054,14 @@
     done
 qed
 
-lemma%important (in sigma_finite_measure) real_RN_deriv:
+proposition (in sigma_finite_measure) real_RN_deriv:
   assumes "finite_measure N"
   assumes ac: "absolutely_continuous M N" "sets N = sets M"
   obtains D where "D \<in> borel_measurable M"
     and "AE x in M. RN_deriv M N x = ennreal (D x)"
     and "AE x in N. 0 < D x"
     and "\<And>x. 0 \<le> D x"
-proof%unimportant
+proof
   interpret N: finite_measure N by fact
 
   note RN = borel_measurable_RN_deriv density_RN_deriv[OF ac]
diff -r 2444c8b85aac -r 0c3dcb3a17f6 src/HOL/Analysis/Regularity.thy
--- a/src/HOL/Analysis/Regularity.thy	Wed Jan 23 17:20:35 2019 +0100
+++ b/src/HOL/Analysis/Regularity.thy	Thu Jan 24 00:28:29 2019 +0000
@@ -4,11 +4,12 @@
 
 section \<open>Regularity of Measures\<close>
 
-theory Regularity (* FIX suggestion to rename to e.g. RegularityMeasures  *)
+theory Regularity (* FIX suggestion to rename  e.g. RegularityMeasures and/ or move as
+this theory consists of 1 result only  *)
 imports Measure_Space Borel_Space
 begin
 
-lemma%important (*FIX needs name *)
+theorem (*FIX needs name *)
   fixes M::"'a::{second_countable_topology, complete_space} measure"
   assumes sb: "sets M = sets borel"
   assumes "emeasure M (space M) \<noteq> \<infinity>"
@@ -17,7 +18,7 @@
     (SUP K \<in> {K. K \<subseteq> B \<and> compact K}. emeasure M K)" (is "?inner B")
   and outer_regular: "emeasure M B =
     (INF U \<in> {U. B \<subseteq> U \<and> open U}. emeasure M U)" (is "?outer B")
-proof%unimportant -
+proof -
   have Us: "UNIV = space M" by (metis assms(1) sets_eq_imp_space_eq space_borel)
   hence sU: "space M = UNIV" by simp
   interpret finite_measure M by rule fact