# HG changeset patch
# User immler
# Date 1531208315 -7200
# Node ID 67bb59e49834ba962abf07a8d78420ff400a9a55
# Parent  96a49db47c9743b51b6a95b22ed241188361f377
make theorem, corollary, and proposition %important for HOL-Analysis manual

diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Mon Jul 09 21:55:40 2018 +0100
+++ b/src/HOL/Analysis/Connected.thy	Tue Jul 10 09:38:35 2018 +0200
@@ -776,12 +776,12 @@
 
 subsection \<open>Intersecting chains of compact sets and the Baire property\<close>
 
-proposition%important bounded_closed_chain:
+proposition bounded_closed_chain:
   fixes \<F> :: "'a::heine_borel set set"
   assumes "B \<in> \<F>" "bounded B" and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> closed S" and "{} \<notin> \<F>"
       and chain: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
     shows "\<Inter>\<F> \<noteq> {}"
-proof%unimportant -
+proof -
   have "B \<inter> \<Inter>\<F> \<noteq> {}"
   proof (rule compact_imp_fip)
     show "compact B" "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
@@ -824,12 +824,12 @@
   then show ?thesis by blast
 qed
 
-corollary%important compact_chain:
+corollary compact_chain:
   fixes \<F> :: "'a::heine_borel set set"
   assumes "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" "{} \<notin> \<F>"
           "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
     shows "\<Inter> \<F> \<noteq> {}"
-proof%unimportant (cases "\<F> = {}")
+proof (cases "\<F> = {}")
   case True
   then show ?thesis by auto
 next
@@ -852,12 +852,12 @@
 qed
 
 text\<open>The Baire property of dense sets\<close>
-theorem%important Baire:
+theorem Baire:
   fixes S::"'a::{real_normed_vector,heine_borel} set"
   assumes "closed S" "countable \<G>"
       and ope: "\<And>T. T \<in> \<G> \<Longrightarrow> openin (subtopology euclidean S) T \<and> S \<subseteq> closure T"
  shows "S \<subseteq> closure(\<Inter>\<G>)"
-proof%unimportant (cases "\<G> = {}")
+proof (cases "\<G> = {}")
   case True
   then show ?thesis
     using closure_subset by auto
@@ -2443,11 +2443,11 @@
   ultimately show ?thesis using that by blast
 qed
 
-corollary%important compact_uniformly_continuous:
+corollary compact_uniformly_continuous:
   fixes f :: "'a :: metric_space \<Rightarrow> 'b :: metric_space"
   assumes f: "continuous_on S f" and S: "compact S"
   shows "uniformly_continuous_on S f"
-  using%unimportant f
+  using f
     unfolding continuous_on_iff uniformly_continuous_on_def
     by (force intro: compact_uniformly_equicontinuous [OF S, of "{f}"])
 
@@ -2929,11 +2929,11 @@
 
 subsection \<open>Separation between points and sets\<close>
 
-lemma%important separate_point_closed:
+proposition separate_point_closed:
   fixes s :: "'a::heine_borel set"
   assumes "closed s" and "a \<notin> s"
   shows "\<exists>d>0. \<forall>x\<in>s. d \<le> dist a x"
-proof%unimportant (cases "s = {}")
+proof (cases "s = {}")
   case True
   then show ?thesis by(auto intro!: exI[where x=1])
 next
@@ -2944,12 +2944,12 @@
     by blast
 qed
 
-lemma%important separate_compact_closed:
+proposition separate_compact_closed:
   fixes s t :: "'a::heine_borel set"
   assumes "compact s"
     and t: "closed t" "s \<inter> t = {}"
   shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
-proof%unimportant cases
+proof cases
   assume "s \<noteq> {} \<and> t \<noteq> {}"
   then have "s \<noteq> {}" "t \<noteq> {}" by auto
   let ?inf = "\<lambda>x. infdist x t"
@@ -2964,27 +2964,27 @@
   ultimately show ?thesis by auto
 qed (auto intro!: exI[of _ 1])
 
-lemma%important separate_closed_compact:
+proposition separate_closed_compact:
   fixes s t :: "'a::heine_borel set"
   assumes "closed s"
     and "compact t"
     and "s \<inter> t = {}"
   shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
-proof%unimportant -
+proof -
   have *: "t \<inter> s = {}"
     using assms(3) by auto
   show ?thesis
     using separate_compact_closed[OF assms(2,1) *] by (force simp: dist_commute)
 qed
 
-lemma%important compact_in_open_separated:
+proposition compact_in_open_separated:
   fixes A::"'a::heine_borel set"
   assumes "A \<noteq> {}"
   assumes "compact A"
   assumes "open B"
   assumes "A \<subseteq> B"
   obtains e where "e > 0" "{x. infdist x A \<le> e} \<subseteq> B"
-proof%unimportant atomize_elim
+proof atomize_elim
   have "closed (- B)" "compact A" "- B \<inter> A = {}"
     using assms by (auto simp: open_Diff compact_eq_bounded_closed)
   from separate_closed_compact[OF this]
@@ -3959,12 +3959,12 @@
     unfolding complete_def by auto
 qed
 
-lemma%important injective_imp_isometric:
+proposition injective_imp_isometric:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes s: "closed s" "subspace s"
     and f: "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0"
   shows "\<exists>e>0. \<forall>x\<in>s. norm (f x) \<ge> e * norm x"
-proof%unimportant (cases "s \<subseteq> {0::'a}")
+proof (cases "s \<subseteq> {0::'a}")
   case True
   have "norm x \<le> norm (f x)" if "x \<in> s" for x
   proof -
@@ -4032,11 +4032,11 @@
   ultimately show ?thesis by auto
 qed
 
-lemma%important closed_injective_image_subspace:
+proposition closed_injective_image_subspace:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "subspace s" "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0" "closed s"
   shows "closed(f ` s)"
-proof%unimportant -
+proof -
   obtain e where "e > 0" and e: "\<forall>x\<in>s. e * norm x \<le> norm (f x)"
     using injective_imp_isometric[OF assms(4,1,2,3)] by auto
   show ?thesis
@@ -4182,13 +4182,13 @@
 
 subsection \<open>Banach fixed point theorem (not really topological ...)\<close>
 
-theorem%important banach_fix:
+theorem banach_fix:
   assumes s: "complete s" "s \<noteq> {}"
     and c: "0 \<le> c" "c < 1"
     and f: "f ` s \<subseteq> s"
     and lipschitz: "\<forall>x\<in>s. \<forall>y\<in>s. dist (f x) (f y) \<le> c * dist x y"
   shows "\<exists>!x\<in>s. f x = x"
-proof%unimportant -
+proof -
   from c have "1 - c > 0" by simp
 
   from s(2) obtain z0 where z0: "z0 \<in> s" by blast
@@ -4338,13 +4338,13 @@
 
 subsection \<open>Edelstein fixed point theorem\<close>
 
-theorem%important edelstein_fix:
+theorem edelstein_fix:
   fixes s :: "'a::metric_space set"
   assumes s: "compact s" "s \<noteq> {}"
     and gs: "(g ` s) \<subseteq> s"
     and dist: "\<forall>x\<in>s. \<forall>y\<in>s. x \<noteq> y \<longrightarrow> dist (g x) (g y) < dist x y"
   shows "\<exists>!x\<in>s. g x = x"
-proof%unimportant -
+proof -
   let ?D = "(\<lambda>x. (x, x)) ` s"
   have D: "compact ?D" "?D \<noteq> {}"
     by (rule compact_continuous_image)
@@ -4693,10 +4693,10 @@
     done
 qed
 
-proposition%important separable:
+proposition separable:
   fixes S :: "'a:: euclidean_space set"
   obtains T where "countable T" "T \<subseteq> S" "S \<subseteq> closure T"
-proof%unimportant -
+proof -
   obtain \<B> :: "'a:: euclidean_space set set"
     where "countable \<B>"
       and "{} \<notin> \<B>"
@@ -4739,11 +4739,11 @@
   qed
 qed
 
-proposition%important Lindelof:
+proposition Lindelof:
   fixes \<F> :: "'a::euclidean_space set set"
   assumes \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> open S"
   obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
-proof%unimportant -
+proof -
   obtain \<B> :: "'a set set"
     where "countable \<B>" "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
       and \<B>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
@@ -5045,11 +5045,11 @@
 qed
 
 
-proposition%important component_diff_connected:
+proposition component_diff_connected:
   fixes S :: "'a::metric_space set"
   assumes "connected S" "connected U" "S \<subseteq> U" and C: "C \<in> components (U - S)"
   shows "connected(U - C)"
-  using%unimportant \<open>connected S\<close> unfolding connected_closedin_eq not_ex de_Morgan_conj
+  using \<open>connected S\<close> unfolding connected_closedin_eq not_ex de_Morgan_conj
 proof clarify
   fix H3 H4 
   assume clo3: "closedin (subtopology euclidean (U - C)) H3" 
@@ -5175,11 +5175,11 @@
     by (metis (no_types, lifting) \<open>0 < e\<close> \<open>open S\<close> half_gt_zero_iff mem_Collect_eq mem_ball open_contains_ball_eq subsetI)
 qed
 
-proposition%important tendsto_componentwise_iff:
+proposition tendsto_componentwise_iff:
   fixes f :: "_ \<Rightarrow> 'b::euclidean_space"
   shows "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>i \<in> Basis. ((\<lambda>x. (f x \<bullet> i)) \<longlongrightarrow> (l \<bullet> i)) F)"
          (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume ?lhs
   then show ?rhs
     unfolding tendsto_def
diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Continuous_Extension.thy
--- a/src/HOL/Analysis/Continuous_Extension.thy	Mon Jul 09 21:55:40 2018 +0100
+++ b/src/HOL/Analysis/Continuous_Extension.thy	Tue Jul 10 09:38:35 2018 +0200
@@ -13,7 +13,7 @@
 text\<open>A difference from HOL Light: all summations over infinite sets equal zero,
    so the "support" must be made explicit in the summation below!\<close>
 
-proposition%important subordinate_partition_of_unity:
+proposition subordinate_partition_of_unity:
   fixes S :: "'a :: euclidean_space set"
   assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
       and fin: "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. U \<inter> V \<noteq> {}}"
@@ -22,7 +22,7 @@
       and "\<And>x U. \<lbrakk>U \<in> \<C>; x \<in> S; x \<notin> U\<rbrakk> \<Longrightarrow> F U x = 0"
       and "\<And>x. x \<in> S \<Longrightarrow> supp_sum (\<lambda>W. F W x) \<C> = 1"
       and "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. F U x \<noteq> 0}"
-proof%unimportant (cases "\<exists>W. W \<in> \<C> \<and> S \<subseteq> W")
+proof (cases "\<exists>W. W \<in> \<C> \<and> S \<subseteq> W")
   case True
     then obtain W where "W \<in> \<C>" "S \<subseteq> W" by metis
     then show ?thesis
@@ -283,7 +283,7 @@
           "\<And>x. f x = b \<longleftrightarrow> x \<in> T"
 using assms by (auto intro: Urysohn_local_strong [of UNIV S T])
 
-proposition%important Urysohn:
+proposition Urysohn:
   assumes US: "closed S"
       and UT: "closed T"
       and "S \<inter> T = {}"
@@ -292,7 +292,7 @@
           "\<And>x. f x \<in> closed_segment a b"
           "\<And>x. x \<in> S \<Longrightarrow> f x = a"
           "\<And>x. x \<in> T \<Longrightarrow> f x = b"
-using%unimportant assms by (auto intro: Urysohn_local [of UNIV S T a b])
+  using assms by (auto intro: Urysohn_local [of UNIV S T a b])
 
 
 subsection\<open>The Dugundji extension theorem and Tietze variants as corollaries\<close>
@@ -300,14 +300,14 @@
 text%important\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367.
 https://projecteuclid.org/euclid.pjm/1103052106\<close>
 
-theorem%important Dugundji:
+theorem Dugundji:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
   assumes "convex C" "C \<noteq> {}"
       and cloin: "closedin (subtopology euclidean U) S"
       and contf: "continuous_on S f" and "f ` S \<subseteq> C"
   obtains g where "continuous_on U g" "g ` U \<subseteq> C"
                   "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
   case True then show thesis
     apply (rule_tac g="\<lambda>x. SOME y. y \<in> C" in that)
       apply (rule continuous_intros)
@@ -475,7 +475,7 @@
 qed
 
 
-corollary%important Tietze:
+corollary Tietze:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
   assumes "continuous_on S f"
       and "closedin (subtopology euclidean U) S"
@@ -483,7 +483,7 @@
       and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> B"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
                   "\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> B"
-using%unimportant assms
+  using assms
 by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f])
 
 corollary Tietze_closed_interval:
diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Continuum_Not_Denumerable.thy
--- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Mon Jul 09 21:55:40 2018 +0100
+++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Tue Jul 10 09:38:35 2018 +0200
@@ -33,8 +33,8 @@
   Nested Interval Property.
 \<close>
 
-theorem%important real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
-proof%unimportant
+theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
+proof
   assume "\<exists>f::nat \<Rightarrow> real. surj f"
   then obtain f :: "nat \<Rightarrow> real" where "surj f" ..
 
diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Jul 09 21:55:40 2018 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Jul 10 09:38:35 2018 +0200
@@ -2005,9 +2005,9 @@
   shows "c *\<^sub>R x \<in> cone hull S"
   by (metis assms cone_cone_hull hull_inc mem_cone)
 
-proposition%important cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
+proposition cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
   (is "?lhs = ?rhs")
-proof%unimportant -
+proof -
   {
     fix x
     assume "x \<in> ?rhs"
@@ -2089,7 +2089,7 @@
    "~ affine_dependent s \<Longrightarrow> ~ affine_dependent(s - t)"
 by (meson Diff_subset affine_dependent_subset)
 
-proposition%important affine_dependent_explicit:
+proposition affine_dependent_explicit:
   "affine_dependent p \<longleftrightarrow>
     (\<exists>S u. finite S \<and> S \<subseteq> p \<and> sum u S = 0 \<and> (\<exists>v\<in>S. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) S = 0)"
 proof -
@@ -2524,7 +2524,7 @@
 
 subsubsection%unimportant \<open>Explicit expression for convex hull\<close>
 
-proposition%important convex_hull_indexed:
+proposition convex_hull_indexed:
   fixes S :: "'a::real_vector set"
   shows "convex hull S =
     {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> S) \<and>
@@ -4020,11 +4020,11 @@
     by (auto simp: convex_hull_explicit)
 qed
 
-theorem%important caratheodory:
+theorem caratheodory:
   "convex hull p =
     {x::'a::euclidean_space. \<exists>s. finite s \<and> s \<subseteq> p \<and>
       card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s}"
-proof%unimportant safe
+proof safe
   fix x
   assume "x \<in> convex hull p"
   then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1"
@@ -5871,10 +5871,10 @@
     done
 qed
 
-theorem%important radon:
+theorem radon:
   assumes "affine_dependent c"
   obtains m p where "m \<subseteq> c" "p \<subseteq> c" "m \<inter> p = {}" "(convex hull m) \<inter> (convex hull p) \<noteq> {}"
-proof%unimportant -
+proof -
   from assms[unfolded affine_dependent_explicit]
   obtain s u where
       "finite s" "s \<subseteq> c" "sum u s = 0" "\<exists>v\<in>s. u v \<noteq> 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0"
@@ -5965,12 +5965,12 @@
   qed 
 qed
 
-theorem%important helly:
+theorem helly:
   fixes f :: "'a::euclidean_space set set"
   assumes "card f \<ge> DIM('a) + 1" "\<forall>s\<in>f. convex s"
     and "\<And>t. \<lbrakk>t\<subseteq>f; card t = DIM('a) + 1\<rbrakk> \<Longrightarrow> \<Inter>t \<noteq> {}"
   shows "\<Inter>f \<noteq> {}"
-  apply%unimportant (rule helly_induct)
+  apply (rule helly_induct)
   using assms
   apply auto
   done
diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/L2_Norm.thy
--- a/src/HOL/Analysis/L2_Norm.thy	Mon Jul 09 21:55:40 2018 +0100
+++ b/src/HOL/Analysis/L2_Norm.thy	Tue Jul 10 09:38:35 2018 +0200
@@ -73,9 +73,9 @@
   unfolding L2_set_def
   by (simp add: sum_nonneg sum_nonneg_eq_0_iff)
 
-lemma %important L2_set_triangle_ineq:
+proposition L2_set_triangle_ineq:
   "L2_set (\<lambda>i. f i + g i) A \<le> L2_set f A + L2_set g A"
-proof %unimportant (cases "finite A")
+proof (cases "finite A")
   case False
   thus ?thesis by simp
 next
diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Mon Jul 09 21:55:40 2018 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Tue Jul 10 09:38:35 2018 +0200
@@ -377,11 +377,11 @@
 subsection \<open>Archimedean properties and useful consequences\<close>
 
 text\<open>Bernoulli's inequality\<close>
-proposition%important Bernoulli_inequality:
+proposition Bernoulli_inequality:
   fixes x :: real
   assumes "-1 \<le> x"
     shows "1 + n * x \<le> (1 + x) ^ n"
-proof%unimportant (induct n)
+proof (induct n)
   case 0
   then show ?case by simp
 next
diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Mon Jul 09 21:55:40 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy	Tue Jul 10 09:38:35 2018 +0200
@@ -1513,7 +1513,7 @@
   "f \<in> measurable M N \<Longrightarrow> A \<in> null_sets (distr M N f) \<longleftrightarrow> f -` A \<inter> space M \<in> null_sets M \<and> A \<in> sets N"
   by (auto simp add: null_sets_def emeasure_distr)
 
-lemma%important distr_distr:
+proposition distr_distr:
   "g \<in> measurable N L \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> distr (distr M N f) L g = distr M L (g \<circ> f)"
   by (auto simp add: emeasure_distr measurable_space
            intro!: arg_cong[where f="emeasure M"] measure_eqI)
@@ -2804,11 +2804,11 @@
   qed auto
 qed
 
-lemma%important unsigned_Hahn_decomposition:
+proposition unsigned_Hahn_decomposition:
   assumes [simp]: "sets N = sets M" and [measurable]: "A \<in> sets M"
     and [simp]: "emeasure M A \<noteq> top" "emeasure N A \<noteq> top"
   shows "\<exists>Y\<in>sets M. Y \<subseteq> A \<and> (\<forall>X\<in>sets M. X \<subseteq> Y \<longrightarrow> N X \<le> M X) \<and> (\<forall>X\<in>sets M. X \<subseteq> A \<longrightarrow> X \<inter> Y = {} \<longrightarrow> M X \<le> N X)"
-proof%unimportant -
+proof -
   have "\<exists>Y\<in>sets (restrict_space M A).
     (\<forall>X\<in>sets (restrict_space M A). X \<subseteq> Y \<longrightarrow> (restrict_space N A) X \<le> (restrict_space M A) X) \<and>
     (\<forall>X\<in>sets (restrict_space M A). X \<inter> Y = {} \<longrightarrow> (restrict_space M A) X \<le> (restrict_space N A) X)"
@@ -2867,8 +2867,8 @@
 
 end
 
-lemma%important le_measure: "sets M = sets N \<Longrightarrow> M \<le> N \<longleftrightarrow> (\<forall>A\<in>sets M. emeasure M A \<le> emeasure N A)"
-  apply%unimportant -
+proposition le_measure: "sets M = sets N \<Longrightarrow> M \<le> N \<longleftrightarrow> (\<forall>A\<in>sets M. emeasure M A \<le> emeasure N A)"
+  apply -
   apply (auto simp: le_measure_iff le_fun_def dest: sets_eq_imp_space_eq)
   subgoal for X
     by (cases "X \<in> sets M") (auto simp: emeasure_notin_sets)
diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Norm_Arith.thy
--- a/src/HOL/Analysis/Norm_Arith.thy	Mon Jul 09 21:55:40 2018 +0100
+++ b/src/HOL/Analysis/Norm_Arith.thy	Tue Jul 10 09:38:35 2018 +0200
@@ -138,7 +138,7 @@
 
 text \<open>Hence more metric properties.\<close>
 
-lemma%important dist_triangle_add:
+proposition dist_triangle_add:
   fixes x y x' y' :: "'a::real_normed_vector"
   shows "dist (x + y) (x' + y') \<le> dist x x' + dist y y'"
   by norm
diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Mon Jul 09 21:55:40 2018 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Tue Jul 10 09:38:35 2018 +0200
@@ -1964,11 +1964,11 @@
   "2 \<le> DIM('N::euclidean_space) \<Longrightarrow> connected(- {a::'N})"
   by (simp add: path_connected_punctured_universe path_connected_imp_connected)
 
-lemma%important path_connected_sphere:
+proposition path_connected_sphere:
   fixes a :: "'a :: euclidean_space"
   assumes "2 \<le> DIM('a)"
   shows "path_connected(sphere a r)"
-proof%unimportant (cases r "0::real" rule: linorder_cases)
+proof (cases r "0::real" rule: linorder_cases)
   case less
   then show ?thesis
     by (simp add: path_connected_empty)
@@ -2289,23 +2289,23 @@
     using path_connected_translation by metis
 qed
 
-lemma%important path_connected_annulus:
+proposition path_connected_annulus:
   fixes a :: "'N::euclidean_space"
   assumes "2 \<le> DIM('N)"
   shows "path_connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
         "path_connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
         "path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
         "path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> r2}"
-  by%unimportant (auto simp: is_interval_def intro!: is_interval_convex convex_imp_path_connected path_connected_2DIM_I [OF assms])
-
-lemma%important connected_annulus:
+  by (auto simp: is_interval_def intro!: is_interval_convex convex_imp_path_connected path_connected_2DIM_I [OF assms])
+
+proposition connected_annulus:
   fixes a :: "'N::euclidean_space"
   assumes "2 \<le> DIM('N::euclidean_space)"
   shows "connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
         "connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
         "connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
         "connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> r2}"
-  by%unimportant (auto simp: path_connected_annulus [OF assms] path_connected_imp_connected)
+  by (auto simp: path_connected_annulus [OF assms] path_connected_imp_connected)
 
 
 subsection%unimportant\<open>Relations between components and path components\<close>
@@ -3302,14 +3302,14 @@
 
 subsection\<open>Condition for an open map's image to contain a ball\<close>
 
-lemma%important ball_subset_open_map_image:
+proposition ball_subset_open_map_image:
   fixes f :: "'a::heine_borel \<Rightarrow> 'b :: {real_normed_vector,heine_borel}"
   assumes contf: "continuous_on (closure S) f"
       and oint: "open (f ` interior S)"
       and le_no: "\<And>z. z \<in> frontier S \<Longrightarrow> r \<le> norm(f z - f a)"
       and "bounded S" "a \<in> S" "0 < r"
     shows "ball (f a) r \<subseteq> f ` S"
-proof%unimportant (cases "f ` S = UNIV")
+proof (cases "f ` S = UNIV")
   case True then show ?thesis by simp
 next
   case False
@@ -3868,26 +3868,26 @@
 
 text%important\<open>So taking equivalence classes under homotopy would give the fundamental group\<close>
 
-proposition%important homotopic_paths_rid:
+proposition homotopic_paths_rid:
     "\<lbrakk>path p; path_image p \<subseteq> s\<rbrakk> \<Longrightarrow> homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p)) p"
-  apply%unimportant (subst homotopic_paths_sym)
+  apply (subst homotopic_paths_sym)
   apply (rule homotopic_paths_reparametrize [where f = "\<lambda>t. if  t \<le> 1 / 2 then 2 *\<^sub>R t else 1"])
   apply (simp_all del: le_divide_eq_numeral1)
   apply (subst split_01)
   apply (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def)+
   done
 
-proposition%important homotopic_paths_lid:
+proposition homotopic_paths_lid:
    "\<lbrakk>path p; path_image p \<subseteq> s\<rbrakk> \<Longrightarrow> homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p) p"
-using%unimportant homotopic_paths_rid [of "reversepath p" s]
+  using homotopic_paths_rid [of "reversepath p" s]
   by (metis homotopic_paths_reversepath path_image_reversepath path_reversepath pathfinish_linepath
         pathfinish_reversepath reversepath_joinpaths reversepath_linepath)
 
-proposition%important homotopic_paths_assoc:
+proposition homotopic_paths_assoc:
    "\<lbrakk>path p; path_image p \<subseteq> s; path q; path_image q \<subseteq> s; path r; path_image r \<subseteq> s; pathfinish p = pathstart q;
      pathfinish q = pathstart r\<rbrakk>
     \<Longrightarrow> homotopic_paths s (p +++ (q +++ r)) ((p +++ q) +++ r)"
-  apply%unimportant (subst homotopic_paths_sym)
+  apply (subst homotopic_paths_sym)
   apply (rule homotopic_paths_reparametrize
            [where f = "\<lambda>t. if  t \<le> 1 / 2 then inverse 2 *\<^sub>R t
                            else if  t \<le> 3 / 4 then t - (1 / 4)
@@ -3898,10 +3898,10 @@
   apply (auto simp: joinpaths_def)
   done
 
-proposition%important homotopic_paths_rinv:
+proposition homotopic_paths_rinv:
   assumes "path p" "path_image p \<subseteq> s"
     shows "homotopic_paths s (p +++ reversepath p) (linepath (pathstart p) (pathstart p))"
-proof%unimportant -
+proof -
   have "continuous_on ({0..1} \<times> {0..1}) (\<lambda>x. (subpath 0 (fst x) p +++ reversepath (subpath 0 (fst x) p)) (snd x))"
     using assms
     apply (simp add: joinpaths_def subpath_def reversepath_def path_def del: le_divide_eq_numeral1)
@@ -3921,10 +3921,10 @@
     done
 qed
 
-proposition%important homotopic_paths_linv:
+proposition homotopic_paths_linv:
   assumes "path p" "path_image p \<subseteq> s"
     shows "homotopic_paths s (reversepath p +++ p) (linepath (pathfinish p) (pathfinish p))"
-using%unimportant homotopic_paths_rinv [of "reversepath p" s] assms by simp
+  using homotopic_paths_rinv [of "reversepath p" s] assms by simp
 
 
 subsection\<open>Homotopy of loops without requiring preservation of endpoints\<close>
@@ -3994,14 +3994,14 @@
 
 subsection\<open>Relations between the two variants of homotopy\<close>
 
-proposition%important homotopic_paths_imp_homotopic_loops:
+proposition homotopic_paths_imp_homotopic_loops:
     "\<lbrakk>homotopic_paths s p q; pathfinish p = pathstart p; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> homotopic_loops s p q"
-  by%unimportant (auto simp: homotopic_paths_def homotopic_loops_def intro: homotopic_with_mono)
-
-proposition%important homotopic_loops_imp_homotopic_paths_null:
+  by (auto simp: homotopic_paths_def homotopic_loops_def intro: homotopic_with_mono)
+
+proposition homotopic_loops_imp_homotopic_paths_null:
   assumes "homotopic_loops s p (linepath a a)"
     shows "homotopic_paths s p (linepath (pathstart p) (pathstart p))"
-proof%unimportant -
+proof -
   have "path p" by (metis assms homotopic_loops_imp_path)
   have ploop: "pathfinish p = pathstart p" by (metis assms homotopic_loops_imp_loop)
   have pip: "path_image p \<subseteq> s" by (metis assms homotopic_loops_imp_subset)
@@ -4069,12 +4069,12 @@
     by (blast intro: homotopic_paths_trans)
 qed
 
-proposition%important homotopic_loops_conjugate:
+proposition homotopic_loops_conjugate:
   fixes s :: "'a::real_normed_vector set"
   assumes "path p" "path q" and pip: "path_image p \<subseteq> s" and piq: "path_image q \<subseteq> s"
       and papp: "pathfinish p = pathstart q" and qloop: "pathfinish q = pathstart q"
     shows "homotopic_loops s (p +++ q +++ reversepath p) q"
-proof%unimportant -
+proof -
   have contp: "continuous_on {0..1} p"  using \<open>path p\<close> [unfolded path_def] by blast
   have contq: "continuous_on {0..1} q"  using \<open>path q\<close> [unfolded path_def] by blast
   have c1: "continuous_on ({0..1} \<times> {0..1}) (\<lambda>x. p ((1 - fst x) * snd x + fst x))"
@@ -4326,10 +4326,10 @@
     using homotopic_join_subpaths2 by blast
 qed
 
-proposition%important homotopic_join_subpaths:
+proposition homotopic_join_subpaths:
    "\<lbrakk>path g; path_image g \<subseteq> s; u \<in> {0..1}; v \<in> {0..1}; w \<in> {0..1}\<rbrakk>
     \<Longrightarrow> homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
-apply%unimportant (rule le_cases3 [of u v w])
+  apply (rule le_cases3 [of u v w])
 using homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3 by metis+
 
 text\<open>Relating homotopy of trivial loops to path-connectedness.\<close>
@@ -5043,7 +5043,7 @@
 
 subsection\<open>Sort of induction principle for connected sets\<close>
 
-lemma%important connected_induction:
+proposition connected_induction:
   assumes "connected S"
       and opD: "\<And>T a. \<lbrakk>openin (subtopology euclidean S) T; a \<in> T\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> T \<and> P z"
       and opI: "\<And>a. a \<in> S
@@ -5051,7 +5051,7 @@
                      (\<forall>x \<in> T. \<forall>y \<in> T. P x \<and> P y \<and> Q x \<longrightarrow> Q y)"
       and etc: "a \<in> S" "b \<in> S" "P a" "P b" "Q a"
     shows "Q b"
-proof%unimportant -
+proof -
   have 1: "openin (subtopology euclidean S)
              {b. \<exists>T. openin (subtopology euclidean S) T \<and>
                      b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> Q x)}"
@@ -5142,14 +5142,14 @@
 
 subsection\<open>Basic properties of local compactness\<close>
 
-lemma%important locally_compact:
+proposition locally_compact:
   fixes s :: "'a :: metric_space set"
   shows
     "locally compact s \<longleftrightarrow>
      (\<forall>x \<in> s. \<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and>
                     openin (subtopology euclidean s) u \<and> compact v)"
      (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume ?lhs
   then show ?rhs
     apply clarify
@@ -5696,12 +5696,12 @@
     by (metis \<open>U = S \<inter> V\<close> inf.bounded_iff openin_imp_subset that)
 qed
 
-corollary%important Sura_Bura:
+corollary Sura_Bura:
   fixes S :: "'a::euclidean_space set"
   assumes "locally compact S" "C \<in> components S" "compact C"
   shows "C = \<Inter> {K. C \<subseteq> K \<and> compact K \<and> openin (subtopology euclidean S) K}"
          (is "C = ?rhs")
-proof%unimportant
+proof
   show "?rhs \<subseteq> C"
   proof (clarsimp, rule ccontr)
     fix x
@@ -5831,17 +5831,17 @@
     by (metis assms(1) assms(2) assms(3) mem_Collect_eq path_component_subset path_connected_path_component)
 qed
 
-proposition%important locally_path_connected:
+proposition locally_path_connected:
   "locally path_connected S \<longleftrightarrow>
    (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
           \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v))"
-by%unimportant (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
-
-proposition%important locally_path_connected_open_path_component:
+  by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
+
+proposition locally_path_connected_open_path_component:
   "locally path_connected S \<longleftrightarrow>
    (\<forall>t x. openin (subtopology euclidean S) t \<and> x \<in> t
           \<longrightarrow> openin (subtopology euclidean S) (path_component_set t x))"
-by%unimportant (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
+  by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
 
 lemma locally_connected_open_component:
   "locally connected S \<longleftrightarrow>
@@ -5849,14 +5849,14 @@
           \<longrightarrow> openin (subtopology euclidean S) c)"
 by (metis components_iff locally_connected_open_connected_component)
 
-proposition%important locally_connected_im_kleinen:
+proposition locally_connected_im_kleinen:
   "locally connected S \<longleftrightarrow>
    (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
        \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and>
                 x \<in> u \<and> u \<subseteq> v \<and>
                 (\<forall>y. y \<in> u \<longrightarrow> (\<exists>c. connected c \<and> c \<subseteq> v \<and> x \<in> c \<and> y \<in> c))))"
    (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume ?lhs
   then show ?rhs
     by (fastforce simp add: locally_connected)
@@ -5890,7 +5890,7 @@
     done
 qed
 
-proposition%important locally_path_connected_im_kleinen:
+proposition locally_path_connected_im_kleinen:
   "locally path_connected S \<longleftrightarrow>
    (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
        \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and>
@@ -5898,7 +5898,7 @@
                 (\<forall>y. y \<in> u \<longrightarrow> (\<exists>p. path p \<and> path_image p \<subseteq> v \<and>
                                 pathstart p = x \<and> pathfinish p = y))))"
    (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume ?lhs
   then show ?rhs
     apply (simp add: locally_path_connected path_connected_def)
@@ -6048,13 +6048,13 @@
   shows "open S \<Longrightarrow> path_component_set S x = connected_component_set S x"
 by (simp add: open_path_connected_component)
 
-proposition%important locally_connected_quotient_image:
+proposition locally_connected_quotient_image:
   assumes lcS: "locally connected S"
       and oo: "\<And>T. T \<subseteq> f ` S
                 \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow>
                     openin (subtopology euclidean (f ` S)) T"
     shows "locally connected (f ` S)"
-proof%unimportant (clarsimp simp: locally_connected_open_component)
+proof (clarsimp simp: locally_connected_open_component)
   fix U C
   assume opefSU: "openin (subtopology euclidean (f ` S)) U" and "C \<in> components U"
   then have "C \<subseteq> U" "U \<subseteq> f ` S"
@@ -6114,12 +6114,12 @@
 qed
 
 text\<open>The proof resembles that above but is not identical!\<close>
-proposition%important locally_path_connected_quotient_image:
+proposition locally_path_connected_quotient_image:
   assumes lcS: "locally path_connected S"
       and oo: "\<And>T. T \<subseteq> f ` S
                 \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow> openin (subtopology euclidean (f ` S)) T"
     shows "locally path_connected (f ` S)"
-proof%unimportant (clarsimp simp: locally_path_connected_open_path_component)
+proof (clarsimp simp: locally_path_connected_open_path_component)
   fix U y
   assume opefSU: "openin (subtopology euclidean (f ` S)) U" and "y \<in> U"
   then have "path_component_set U y \<subseteq> U" "U \<subseteq> f ` S"
@@ -6345,7 +6345,7 @@
     by (rule that [OF \<open>linear f\<close> \<open>f ` S \<subseteq> T\<close>])
 qed
 
-proposition%important isometries_subspaces:
+proposition isometries_subspaces:
   fixes S :: "'a::euclidean_space set"
     and T :: "'b::euclidean_space set"
   assumes S: "subspace S"
@@ -6356,7 +6356,7 @@
                     "\<And>x. x \<in> T \<Longrightarrow> norm(g x) = norm x"
                     "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
                     "\<And>x. x \<in> T \<Longrightarrow> f(g x) = x"
-proof%unimportant -
+proof -
   obtain B where "B \<subseteq> S" and Borth: "pairwise orthogonal B"
              and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
              and "independent B" "finite B" "card B = dim S" "span B = S"
@@ -7815,7 +7815,7 @@
   qed
 qed
 
-proposition%important homeomorphism_moving_points_exists:
+proposition homeomorphism_moving_points_exists:
   fixes S :: "'a::euclidean_space set"
   assumes 2: "2 \<le> DIM('a)" "open S" "connected S" "S \<subseteq> T" "finite K"
       and KS: "\<And>i. i \<in> K \<Longrightarrow> x i \<in> S \<and> y i \<in> S"
@@ -7823,7 +7823,7 @@
       and S: "S \<subseteq> T" "T \<subseteq> affine hull S" "connected S"
   obtains f g where "homeomorphism T T f g" "\<And>i. i \<in> K \<Longrightarrow> f(x i) = y i"
                     "{x. ~ (f x = x \<and> g x = x)} \<subseteq> S" "bounded {x. (~ (f x = x \<and> g x = x))}"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
   case True
   then show ?thesis
     using KS homeomorphism_ident that by fastforce
@@ -8082,12 +8082,12 @@
   qed
 qed
 
-proposition%important homeomorphism_grouping_points_exists:
+proposition homeomorphism_grouping_points_exists:
   fixes S :: "'a::euclidean_space set"
   assumes "open U" "open S" "connected S" "U \<noteq> {}" "finite K" "K \<subseteq> S" "U \<subseteq> S" "S \<subseteq> T"
   obtains f g where "homeomorphism T T f g" "{x. (~ (f x = x \<and> g x = x))} \<subseteq> S"
                     "bounded {x. (~ (f x = x \<and> g x = x))}" "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U"
-proof%unimportant (cases "2 \<le> DIM('a)")
+proof (cases "2 \<le> DIM('a)")
   case True
   have TS: "T \<subseteq> affine hull S"
     using affine_hull_open assms by blast
@@ -8364,13 +8364,13 @@
   qed
 qed
 
-proposition%important nullhomotopic_from_sphere_extension:
+proposition nullhomotopic_from_sphere_extension:
   fixes f :: "'M::euclidean_space \<Rightarrow> 'a::real_normed_vector"
   shows  "(\<exists>c. homotopic_with (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)) \<longleftrightarrow>
           (\<exists>g. continuous_on (cball a r) g \<and> g ` (cball a r) \<subseteq> S \<and>
                (\<forall>x \<in> sphere a r. g x = f x))"
          (is "?lhs = ?rhs")
-proof%unimportant (cases r "0::real" rule: linorder_cases)
+proof (cases r "0::real" rule: linorder_cases)
   case equal
   then show ?thesis
     apply (auto simp: homotopic_with)
diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Product_Vector.thy
--- a/src/HOL/Analysis/Product_Vector.thy	Mon Jul 09 21:55:40 2018 +0100
+++ b/src/HOL/Analysis/Product_Vector.thy	Tue Jul 10 09:38:35 2018 +0200
@@ -314,11 +314,11 @@
 
 subsubsection%unimportant \<open>Pair operations are linear\<close>
 
-lemma%important bounded_linear_fst: "bounded_linear fst"
+proposition bounded_linear_fst: "bounded_linear fst"
   using fst_add fst_scaleR
   by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
 
-lemma%important bounded_linear_snd: "bounded_linear snd"
+proposition bounded_linear_snd: "bounded_linear snd"
   using snd_add snd_scaleR
   by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
 
@@ -354,10 +354,10 @@
 
 subsubsection%unimportant \<open>Frechet derivatives involving pairs\<close>
 
-lemma%important has_derivative_Pair [derivative_intros]:
+proposition has_derivative_Pair [derivative_intros]:
   assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
   shows "((\<lambda>x. (f x, g x)) has_derivative (\<lambda>h. (f' h, g' h))) (at x within s)"
-proof%unimportant (rule has_derivativeI_sandwich[of 1])
+proof (rule has_derivativeI_sandwich[of 1])
   show "bounded_linear (\<lambda>h. (f' h, g' h))"
     using f g by (intro bounded_linear_Pair has_derivative_bounded_linear)
   let ?Rf = "\<lambda>y. f y - f x - f' (y - x)"
diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Sigma_Algebra.thy
--- a/src/HOL/Analysis/Sigma_Algebra.thy	Mon Jul 09 21:55:40 2018 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Tue Jul 10 09:38:35 2018 +0200
@@ -146,13 +146,13 @@
   "a \<in> M \<Longrightarrow> \<Omega> - a \<in> M"
   by auto
 
-lemma%important algebra_iff_Un:
+proposition algebra_iff_Un:
   "algebra \<Omega> M \<longleftrightarrow>
     M \<subseteq> Pow \<Omega> \<and>
     {} \<in> M \<and>
     (\<forall>a \<in> M. \<Omega> - a \<in> M) \<and>
     (\<forall>a \<in> M. \<forall> b \<in> M. a \<union> b \<in> M)" (is "_ \<longleftrightarrow> ?Un")
-proof%unimportant
+proof
   assume "algebra \<Omega> M"
   then interpret algebra \<Omega> M .
   show ?Un using sets_into_space by auto
@@ -173,12 +173,12 @@
   show "algebra \<Omega> M" proof qed fact
 qed
 
-lemma%important algebra_iff_Int:
+proposition algebra_iff_Int:
      "algebra \<Omega> M \<longleftrightarrow>
        M \<subseteq> Pow \<Omega> & {} \<in> M &
        (\<forall>a \<in> M. \<Omega> - a \<in> M) &
        (\<forall>a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)" (is "_ \<longleftrightarrow> ?Int")
-proof%unimportant
+proof
   assume "algebra \<Omega> M"
   then interpret algebra \<Omega> M .
   show ?Int using sets_into_space by auto
@@ -1433,7 +1433,7 @@
 text%important \<open>The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras
 generated by a generator closed under intersection.\<close>
 
-lemma%important sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
+proposition sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
   assumes "Int_stable G"
     and closed: "G \<subseteq> Pow \<Omega>"
     and A: "A \<in> sigma_sets \<Omega> G"
@@ -1442,7 +1442,7 @@
     and compl: "\<And>A. A \<in> sigma_sets \<Omega> G \<Longrightarrow> P A \<Longrightarrow> P (\<Omega> - A)"
     and union: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sigma_sets \<Omega> G \<Longrightarrow> (\<And>i. P (A i)) \<Longrightarrow> P (\<Union>i::nat. A i)"
   shows "P A"
-proof%unimportant -
+proof -
   let ?D = "{ A \<in> sigma_sets \<Omega> G. P A }"
   interpret sigma_algebra \<Omega> "sigma_sets \<Omega> G"
     using closed by (rule sigma_algebra_sigma_sets)
@@ -1633,12 +1633,12 @@
 
 subsubsection \<open>Constructing simple @{typ "'a measure"}\<close>
 
-lemma%important emeasure_measure_of:
+proposition emeasure_measure_of:
   assumes M: "M = measure_of \<Omega> A \<mu>"
   assumes ms: "A \<subseteq> Pow \<Omega>" "positive (sets M) \<mu>" "countably_additive (sets M) \<mu>"
   assumes X: "X \<in> sets M"
   shows "emeasure M X = \<mu> X"
-proof%unimportant -
+proof -
   interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" by (rule sigma_algebra_sigma_sets) fact
   have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>"
     using ms M by (simp add: measure_space_def sigma_algebra_sigma_sets)
diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Mon Jul 09 21:55:40 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Tue Jul 10 09:38:35 2018 +0200
@@ -5063,12 +5063,12 @@
 
 subsection\<open>Connectedness of the intersection of a chain\<close>
 
-proposition%important connected_chain:
+proposition connected_chain:
   fixes \<F> :: "'a :: euclidean_space set set"
   assumes cc: "\<And>S. S \<in> \<F> \<Longrightarrow> compact S \<and> connected S"
       and linear: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
   shows "connected(\<Inter>\<F>)"
-proof%unimportant (cases "\<F> = {}")
+proof (cases "\<F> = {}")
   case True then show ?thesis
     by auto
 next
@@ -5212,13 +5212,13 @@
       by (meson le_max_iff_disj)
 qed
 
-proposition%important proper_map:
+proposition proper_map:
   fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
   assumes "closedin (subtopology euclidean S) K"
       and com: "\<And>U. \<lbrakk>U \<subseteq> T; compact U\<rbrakk> \<Longrightarrow> compact (S \<inter> f -` U)"
       and "f ` S \<subseteq> T"
     shows "closedin (subtopology euclidean T) (f ` K)"
-proof%unimportant -
+proof -
   have "K \<subseteq> S"
     using assms closedin_imp_subset by metis
   obtain C where "closed C" and Keq: "K = S \<inter> C"
@@ -6708,11 +6708,11 @@
   by (metis a orthogonal_clauses(1,2,4)
       span_induct_alt x)
 
-proposition%important Gram_Schmidt_step:
+proposition Gram_Schmidt_step:
   fixes S :: "'a::euclidean_space set"
   assumes S: "pairwise orthogonal S" and x: "x \<in> span S"
     shows "orthogonal x (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b))"
-proof%unimportant -
+proof -
   have "finite S"
     by (simp add: S pairwise_orthogonal_imp_finite)
   have "orthogonal (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)) x"
@@ -6767,11 +6767,11 @@
 qed
 
 
-proposition%important orthogonal_extension:
+proposition orthogonal_extension:
   fixes S :: "'a::euclidean_space set"
   assumes S: "pairwise orthogonal S"
   obtains U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
-proof%unimportant -
+proof -
   obtain B where "finite B" "span B = span T"
     using basis_subspace_exists [of "span T"] subspace_span by metis
   with orthogonal_extension_aux [of B S]
@@ -6827,13 +6827,13 @@
     done
 qed
 
-proposition%important orthonormal_basis_subspace:
+proposition orthonormal_basis_subspace:
   fixes S :: "'a :: euclidean_space set"
   assumes "subspace S"
   obtains B where "B \<subseteq> S" "pairwise orthogonal B"
               and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
               and "independent B" "card B = dim S" "span B = S"
-proof%unimportant -
+proof -
   obtain B where "0 \<notin> B" "B \<subseteq> S"
              and orth: "pairwise orthogonal B"
              and "independent B" "card B = dim S" "span B = S"
@@ -6864,11 +6864,11 @@
 qed
 
 
-proposition%important orthogonal_to_subspace_exists_gen:
+proposition orthogonal_to_subspace_exists_gen:
   fixes S :: "'a :: euclidean_space set"
   assumes "span S \<subset> span T"
   obtains x where "x \<noteq> 0" "x \<in> span T" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
-proof%unimportant -
+proof -
   obtain B where "B \<subseteq> span S" and orthB: "pairwise orthogonal B"
              and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
              and "independent B" "card B = dim S" "span B = span S"
@@ -6933,10 +6933,10 @@
     by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_base that)
 qed
 
-proposition%important orthogonal_subspace_decomp_exists:
+proposition orthogonal_subspace_decomp_exists:
   fixes S :: "'a :: euclidean_space set"
   obtains y z where "y \<in> span S" "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w" "x = y + z"
-proof%unimportant -
+proof -
   obtain T where "0 \<notin> T" "T \<subseteq> span S" "pairwise orthogonal T" "independent T"
     "card T = dim (span S)" "span T = span S"
     using orthogonal_basis_subspace subspace_span by blast
@@ -7030,11 +7030,11 @@
   qed
 qed
 
-proposition%important dim_orthogonal_sum:
+proposition dim_orthogonal_sum:
   fixes A :: "'a::euclidean_space set"
   assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
     shows "dim(A \<union> B) = dim A + dim B"
-proof%unimportant -
+proof -
   have 1: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
     by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms)
   have "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
@@ -7163,10 +7163,10 @@
 
 subsection\<open>Lower-dimensional affine subsets are nowhere dense\<close>
 
-proposition%important dense_complement_subspace:
+proposition dense_complement_subspace:
   fixes S :: "'a :: euclidean_space set"
   assumes dim_less: "dim T < dim S" and "subspace S" shows "closure(S - T) = S"
-proof%unimportant -
+proof -
   have "closure(S - U) = S" if "dim U < dim S" "U \<subseteq> S" for U
   proof -
     have "span U \<subset> span S"
@@ -7465,7 +7465,7 @@
 
 subsection\<open>Several Variants of Paracompactness\<close>
 
-proposition%important paracompact:
+proposition paracompact:
   fixes S :: "'a :: euclidean_space set"
   assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
   obtains \<C>' where "S \<subseteq> \<Union> \<C>'"
@@ -7473,7 +7473,7 @@
                and "\<And>x. x \<in> S
                        \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and>
                                finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
   case True with that show ?thesis by blast
 next
   case False
@@ -7858,14 +7858,14 @@
 
 subsection\<open>Covering an open set by a countable chain of compact sets\<close>
   
-proposition%important open_Union_compact_subsets:
+proposition open_Union_compact_subsets:
   fixes S :: "'a::euclidean_space set"
   assumes "open S"
   obtains C where "\<And>n. compact(C n)" "\<And>n. C n \<subseteq> S"
                   "\<And>n. C n \<subseteq> interior(C(Suc n))"
                   "\<Union>(range C) = S"
                   "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. K \<subseteq> (C n)"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
   case True
   then show ?thesis
     by (rule_tac C = "\<lambda>n. {}" in that) auto
diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Jul 09 21:55:40 2018 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Jul 10 09:38:35 2018 +0200
@@ -640,7 +640,7 @@
 
 subsubsection \<open>Main properties of open sets\<close>
 
-lemma%important openin_clauses:
+proposition openin_clauses:
   fixes U :: "'a topology"
   shows
     "openin U {}"
@@ -2765,16 +2765,16 @@
 
 subsection \<open>Limits\<close>
 
-lemma%important Lim: "(f \<longlongrightarrow> l) net \<longleftrightarrow> trivial_limit net \<or> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
+proposition Lim: "(f \<longlongrightarrow> l) net \<longleftrightarrow> trivial_limit net \<or> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
   by (auto simp: tendsto_iff trivial_limit_eq)
 
 text \<open>Show that they yield usual definitions in the various cases.\<close>
 
-lemma%important Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
+proposition Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
     (\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> dist (f x) l < e)"
   by (auto simp: tendsto_iff eventually_at_le)
 
-lemma%important Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
+proposition Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
     (\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a  < d \<longrightarrow> dist (f x) l < e)"
   by (auto simp: tendsto_iff eventually_at)
 
@@ -2785,11 +2785,11 @@
   apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
   done
 
-lemma%important Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
+proposition Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
     (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d  \<longrightarrow> dist (f x) l < e)"
   by (auto simp: tendsto_iff eventually_at)
 
-lemma%important Lim_at_infinity: "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)"
+proposition Lim_at_infinity: "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)"
   by (auto simp: tendsto_iff eventually_at_infinity)
 
 corollary Lim_at_infinityI [intro?]:
@@ -3652,12 +3652,12 @@
 
 subsubsection \<open>Bolzano-Weierstrass property\<close>
 
-lemma%important heine_borel_imp_bolzano_weierstrass:
+proposition heine_borel_imp_bolzano_weierstrass:
   assumes "compact s"
     and "infinite t"
     and "t \<subseteq> s"
   shows "\<exists>x \<in> s. x islimpt t"
-proof%unimportant (rule ccontr)
+proof (rule ccontr)
   assume "\<not> (\<exists>x \<in> s. x islimpt t)"
   then obtain f where f: "\<forall>x\<in>s. x \<in> f x \<and> open (f x) \<and> (\<forall>y\<in>t. y \<in> f x \<longrightarrow> y = x)"
     unfolding islimpt_def
@@ -4170,9 +4170,9 @@
     unfolding C_def by (intro exI[of _ "f`T"]) fastforce
 qed
 
-lemma%important countably_compact_imp_compact_second_countable:
+proposition countably_compact_imp_compact_second_countable:
   "countably_compact U \<Longrightarrow> compact (U :: 'a :: second_countable_topology set)"
-proof%unimportant (rule countably_compact_imp_compact)
+proof (rule countably_compact_imp_compact)
   fix T and x :: 'a
   assume "open T" "x \<in> T"
   from topological_basisE[OF is_basis this] obtain b where
@@ -4448,10 +4448,10 @@
   shows "seq_compact U \<longleftrightarrow> compact U"
   using seq_compact_eq_countably_compact countably_compact_eq_compact by blast
 
-lemma%important bolzano_weierstrass_imp_seq_compact:
+proposition bolzano_weierstrass_imp_seq_compact:
   fixes s :: "'a::{t1_space, first_countable_topology} set"
   shows "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> seq_compact s"
-  by%unimportant (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
+  by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
 
 
 subsubsection\<open>Totally bounded\<close>
@@ -4459,10 +4459,10 @@
 lemma cauchy_def: "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N \<longrightarrow> dist (s m) (s n) < e)"
   unfolding Cauchy_def by metis
 
-lemma%important seq_compact_imp_totally_bounded:
+proposition seq_compact_imp_totally_bounded:
   assumes "seq_compact s"
   shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>k. ball x e)"
-proof%unimportant -
+proof -
   { fix e::real assume "e > 0" assume *: "\<And>k. finite k \<Longrightarrow> k \<subseteq> s \<Longrightarrow> \<not> s \<subseteq> (\<Union>x\<in>k. ball x e)"
     let ?Q = "\<lambda>x n r. r \<in> s \<and> (\<forall>m < (n::nat). \<not> (dist (x m) r < e))"
     have "\<exists>x. \<forall>n::nat. ?Q x n (x n)"
@@ -4491,11 +4491,11 @@
 
 subsubsection\<open>Heine-Borel theorem\<close>
 
-lemma%important seq_compact_imp_heine_borel:
+proposition seq_compact_imp_heine_borel:
   fixes s :: "'a :: metric_space set"
   assumes "seq_compact s"
   shows "compact s"
-proof%unimportant -
+proof -
   from seq_compact_imp_totally_bounded[OF \<open>seq_compact s\<close>]
   obtain f where f: "\<forall>e>0. finite (f e) \<and> f e \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>f e. ball x e)"
     unfolding choice_iff' ..
@@ -4536,22 +4536,22 @@
   qed
 qed
 
-lemma%important compact_eq_seq_compact_metric:
+proposition compact_eq_seq_compact_metric:
   "compact (s :: 'a::metric_space set) \<longleftrightarrow> seq_compact s"
   using compact_imp_seq_compact seq_compact_imp_heine_borel by blast
 
-lemma%important compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
+proposition compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
   "compact (S :: 'a::metric_space set) \<longleftrightarrow>
    (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l))"
   unfolding compact_eq_seq_compact_metric seq_compact_def by auto
 
 subsubsection \<open>Complete the chain of compactness variants\<close>
 
-lemma%important compact_eq_bolzano_weierstrass:
+proposition compact_eq_bolzano_weierstrass:
   fixes s :: "'a::metric_space set"
   shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))"
   (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume ?lhs
   then show ?rhs
     using heine_borel_imp_bolzano_weierstrass[of s] by auto
@@ -4561,7 +4561,7 @@
     unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact)
 qed
 
-lemma%important bolzano_weierstrass_imp_bounded:
+proposition bolzano_weierstrass_imp_bounded:
   "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s"
   using compact_imp_bounded unfolding compact_eq_bolzano_weierstrass .
 
@@ -4577,12 +4577,12 @@
   assumes bounded_imp_convergent_subsequence:
     "bounded (range f) \<Longrightarrow> \<exists>l r. strict_mono (r::nat\<Rightarrow>nat) \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
 
-lemma%important bounded_closed_imp_seq_compact:
+proposition bounded_closed_imp_seq_compact:
   fixes s::"'a::heine_borel set"
   assumes "bounded s"
     and "closed s"
   shows "seq_compact s"
-proof%unimportant (unfold seq_compact_def, clarify)
+proof (unfold seq_compact_def, clarify)
   fix f :: "nat \<Rightarrow> 'a"
   assume f: "\<forall>n. f n \<in> s"
   with \<open>bounded s\<close> have "bounded (range f)"
@@ -4807,12 +4807,12 @@
 
 subsubsection \<open>Completeness\<close>
 
-lemma%important (in metric_space) completeI:
+proposition (in metric_space) completeI:
   assumes "\<And>f. \<forall>n. f n \<in> s \<Longrightarrow> Cauchy f \<Longrightarrow> \<exists>l\<in>s. f \<longlonglongrightarrow> l"
   shows "complete s"
   using assms unfolding complete_def by fast
 
-lemma%important (in metric_space) completeE:
+proposition (in metric_space) completeE:
   assumes "complete s" and "\<forall>n. f n \<in> s" and "Cauchy f"
   obtains l where "l \<in> s" and "f \<longlonglongrightarrow> l"
   using assms unfolding complete_def by fast
@@ -4862,10 +4862,10 @@
   then show ?thesis unfolding complete_def by auto
 qed
 
-lemma%important compact_eq_totally_bounded:
+proposition compact_eq_totally_bounded:
   "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))"
     (is "_ \<longleftrightarrow> ?rhs")
-proof%unimportant
+proof
   assume assms: "?rhs"
   then obtain k where k: "\<And>e. 0 < e \<Longrightarrow> finite (k e)" "\<And>e. 0 < e \<Longrightarrow> s \<subseteq> (\<Union>x\<in>k e. ball x e)"
     by (auto simp: choice_iff')
@@ -5069,7 +5069,7 @@
 
 text\<open>Derive the epsilon-delta forms, which we often use as "definitions"\<close>
 
-lemma%important continuous_within_eps_delta:
+proposition continuous_within_eps_delta:
   "continuous (at x within s) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> s.  dist x' x < d --> dist (f x') (f x) < e)"
   unfolding continuous_within and Lim_within  by fastforce
 
diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Jul 09 21:55:40 2018 +0100
+++ b/src/HOL/ROOT	Tue Jul 10 09:38:35 2018 +0200
@@ -58,7 +58,7 @@
   document_files "root.bib" "root.tex"
 
 session "HOL-Analysis" (main timing) in Analysis = HOL +
-  options [document_tags = "%unimportant",
+  options [document_tags = "theorem%important,corollary%important,proposition%important,%unimportant",
     document_variants = "document:manual=-proof,-ML,-unimportant"]
   sessions
     "HOL-Library"