make theorem, corollary, and proposition %important for HOL-Analysis manual
authorimmler
Tue Jul 10 09:38:35 2018 +0200 (10 months ago)
changeset 6860767bb59e49834
parent 68606 96a49db47c97
child 68609 9963bb965a0e
make theorem, corollary, and proposition %important for HOL-Analysis manual
src/HOL/Analysis/Connected.thy
src/HOL/Analysis/Continuous_Extension.thy
src/HOL/Analysis/Continuum_Not_Denumerable.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/L2_Norm.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Measure_Space.thy
src/HOL/Analysis/Norm_Arith.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Product_Vector.thy
src/HOL/Analysis/Sigma_Algebra.thy
src/HOL/Analysis/Starlike.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/Analysis/Connected.thy	Mon Jul 09 21:55:40 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Connected.thy	Tue Jul 10 09:38:35 2018 +0200
     1.3 @@ -776,12 +776,12 @@
     1.4  
     1.5  subsection \<open>Intersecting chains of compact sets and the Baire property\<close>
     1.6  
     1.7 -proposition%important bounded_closed_chain:
     1.8 +proposition bounded_closed_chain:
     1.9    fixes \<F> :: "'a::heine_borel set set"
    1.10    assumes "B \<in> \<F>" "bounded B" and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> closed S" and "{} \<notin> \<F>"
    1.11        and chain: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
    1.12      shows "\<Inter>\<F> \<noteq> {}"
    1.13 -proof%unimportant -
    1.14 +proof -
    1.15    have "B \<inter> \<Inter>\<F> \<noteq> {}"
    1.16    proof (rule compact_imp_fip)
    1.17      show "compact B" "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
    1.18 @@ -824,12 +824,12 @@
    1.19    then show ?thesis by blast
    1.20  qed
    1.21  
    1.22 -corollary%important compact_chain:
    1.23 +corollary compact_chain:
    1.24    fixes \<F> :: "'a::heine_borel set set"
    1.25    assumes "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" "{} \<notin> \<F>"
    1.26            "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
    1.27      shows "\<Inter> \<F> \<noteq> {}"
    1.28 -proof%unimportant (cases "\<F> = {}")
    1.29 +proof (cases "\<F> = {}")
    1.30    case True
    1.31    then show ?thesis by auto
    1.32  next
    1.33 @@ -852,12 +852,12 @@
    1.34  qed
    1.35  
    1.36  text\<open>The Baire property of dense sets\<close>
    1.37 -theorem%important Baire:
    1.38 +theorem Baire:
    1.39    fixes S::"'a::{real_normed_vector,heine_borel} set"
    1.40    assumes "closed S" "countable \<G>"
    1.41        and ope: "\<And>T. T \<in> \<G> \<Longrightarrow> openin (subtopology euclidean S) T \<and> S \<subseteq> closure T"
    1.42   shows "S \<subseteq> closure(\<Inter>\<G>)"
    1.43 -proof%unimportant (cases "\<G> = {}")
    1.44 +proof (cases "\<G> = {}")
    1.45    case True
    1.46    then show ?thesis
    1.47      using closure_subset by auto
    1.48 @@ -2443,11 +2443,11 @@
    1.49    ultimately show ?thesis using that by blast
    1.50  qed
    1.51  
    1.52 -corollary%important compact_uniformly_continuous:
    1.53 +corollary compact_uniformly_continuous:
    1.54    fixes f :: "'a :: metric_space \<Rightarrow> 'b :: metric_space"
    1.55    assumes f: "continuous_on S f" and S: "compact S"
    1.56    shows "uniformly_continuous_on S f"
    1.57 -  using%unimportant f
    1.58 +  using f
    1.59      unfolding continuous_on_iff uniformly_continuous_on_def
    1.60      by (force intro: compact_uniformly_equicontinuous [OF S, of "{f}"])
    1.61  
    1.62 @@ -2929,11 +2929,11 @@
    1.63  
    1.64  subsection \<open>Separation between points and sets\<close>
    1.65  
    1.66 -lemma%important separate_point_closed:
    1.67 +proposition separate_point_closed:
    1.68    fixes s :: "'a::heine_borel set"
    1.69    assumes "closed s" and "a \<notin> s"
    1.70    shows "\<exists>d>0. \<forall>x\<in>s. d \<le> dist a x"
    1.71 -proof%unimportant (cases "s = {}")
    1.72 +proof (cases "s = {}")
    1.73    case True
    1.74    then show ?thesis by(auto intro!: exI[where x=1])
    1.75  next
    1.76 @@ -2944,12 +2944,12 @@
    1.77      by blast
    1.78  qed
    1.79  
    1.80 -lemma%important separate_compact_closed:
    1.81 +proposition separate_compact_closed:
    1.82    fixes s t :: "'a::heine_borel set"
    1.83    assumes "compact s"
    1.84      and t: "closed t" "s \<inter> t = {}"
    1.85    shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
    1.86 -proof%unimportant cases
    1.87 +proof cases
    1.88    assume "s \<noteq> {} \<and> t \<noteq> {}"
    1.89    then have "s \<noteq> {}" "t \<noteq> {}" by auto
    1.90    let ?inf = "\<lambda>x. infdist x t"
    1.91 @@ -2964,27 +2964,27 @@
    1.92    ultimately show ?thesis by auto
    1.93  qed (auto intro!: exI[of _ 1])
    1.94  
    1.95 -lemma%important separate_closed_compact:
    1.96 +proposition separate_closed_compact:
    1.97    fixes s t :: "'a::heine_borel set"
    1.98    assumes "closed s"
    1.99      and "compact t"
   1.100      and "s \<inter> t = {}"
   1.101    shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
   1.102 -proof%unimportant -
   1.103 +proof -
   1.104    have *: "t \<inter> s = {}"
   1.105      using assms(3) by auto
   1.106    show ?thesis
   1.107      using separate_compact_closed[OF assms(2,1) *] by (force simp: dist_commute)
   1.108  qed
   1.109  
   1.110 -lemma%important compact_in_open_separated:
   1.111 +proposition compact_in_open_separated:
   1.112    fixes A::"'a::heine_borel set"
   1.113    assumes "A \<noteq> {}"
   1.114    assumes "compact A"
   1.115    assumes "open B"
   1.116    assumes "A \<subseteq> B"
   1.117    obtains e where "e > 0" "{x. infdist x A \<le> e} \<subseteq> B"
   1.118 -proof%unimportant atomize_elim
   1.119 +proof atomize_elim
   1.120    have "closed (- B)" "compact A" "- B \<inter> A = {}"
   1.121      using assms by (auto simp: open_Diff compact_eq_bounded_closed)
   1.122    from separate_closed_compact[OF this]
   1.123 @@ -3959,12 +3959,12 @@
   1.124      unfolding complete_def by auto
   1.125  qed
   1.126  
   1.127 -lemma%important injective_imp_isometric:
   1.128 +proposition injective_imp_isometric:
   1.129    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   1.130    assumes s: "closed s" "subspace s"
   1.131      and f: "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0"
   1.132    shows "\<exists>e>0. \<forall>x\<in>s. norm (f x) \<ge> e * norm x"
   1.133 -proof%unimportant (cases "s \<subseteq> {0::'a}")
   1.134 +proof (cases "s \<subseteq> {0::'a}")
   1.135    case True
   1.136    have "norm x \<le> norm (f x)" if "x \<in> s" for x
   1.137    proof -
   1.138 @@ -4032,11 +4032,11 @@
   1.139    ultimately show ?thesis by auto
   1.140  qed
   1.141  
   1.142 -lemma%important closed_injective_image_subspace:
   1.143 +proposition closed_injective_image_subspace:
   1.144    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   1.145    assumes "subspace s" "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0" "closed s"
   1.146    shows "closed(f ` s)"
   1.147 -proof%unimportant -
   1.148 +proof -
   1.149    obtain e where "e > 0" and e: "\<forall>x\<in>s. e * norm x \<le> norm (f x)"
   1.150      using injective_imp_isometric[OF assms(4,1,2,3)] by auto
   1.151    show ?thesis
   1.152 @@ -4182,13 +4182,13 @@
   1.153  
   1.154  subsection \<open>Banach fixed point theorem (not really topological ...)\<close>
   1.155  
   1.156 -theorem%important banach_fix:
   1.157 +theorem banach_fix:
   1.158    assumes s: "complete s" "s \<noteq> {}"
   1.159      and c: "0 \<le> c" "c < 1"
   1.160      and f: "f ` s \<subseteq> s"
   1.161      and lipschitz: "\<forall>x\<in>s. \<forall>y\<in>s. dist (f x) (f y) \<le> c * dist x y"
   1.162    shows "\<exists>!x\<in>s. f x = x"
   1.163 -proof%unimportant -
   1.164 +proof -
   1.165    from c have "1 - c > 0" by simp
   1.166  
   1.167    from s(2) obtain z0 where z0: "z0 \<in> s" by blast
   1.168 @@ -4338,13 +4338,13 @@
   1.169  
   1.170  subsection \<open>Edelstein fixed point theorem\<close>
   1.171  
   1.172 -theorem%important edelstein_fix:
   1.173 +theorem edelstein_fix:
   1.174    fixes s :: "'a::metric_space set"
   1.175    assumes s: "compact s" "s \<noteq> {}"
   1.176      and gs: "(g ` s) \<subseteq> s"
   1.177      and dist: "\<forall>x\<in>s. \<forall>y\<in>s. x \<noteq> y \<longrightarrow> dist (g x) (g y) < dist x y"
   1.178    shows "\<exists>!x\<in>s. g x = x"
   1.179 -proof%unimportant -
   1.180 +proof -
   1.181    let ?D = "(\<lambda>x. (x, x)) ` s"
   1.182    have D: "compact ?D" "?D \<noteq> {}"
   1.183      by (rule compact_continuous_image)
   1.184 @@ -4693,10 +4693,10 @@
   1.185      done
   1.186  qed
   1.187  
   1.188 -proposition%important separable:
   1.189 +proposition separable:
   1.190    fixes S :: "'a:: euclidean_space set"
   1.191    obtains T where "countable T" "T \<subseteq> S" "S \<subseteq> closure T"
   1.192 -proof%unimportant -
   1.193 +proof -
   1.194    obtain \<B> :: "'a:: euclidean_space set set"
   1.195      where "countable \<B>"
   1.196        and "{} \<notin> \<B>"
   1.197 @@ -4739,11 +4739,11 @@
   1.198    qed
   1.199  qed
   1.200  
   1.201 -proposition%important Lindelof:
   1.202 +proposition Lindelof:
   1.203    fixes \<F> :: "'a::euclidean_space set set"
   1.204    assumes \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> open S"
   1.205    obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
   1.206 -proof%unimportant -
   1.207 +proof -
   1.208    obtain \<B> :: "'a set set"
   1.209      where "countable \<B>" "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
   1.210        and \<B>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
   1.211 @@ -5045,11 +5045,11 @@
   1.212  qed
   1.213  
   1.214  
   1.215 -proposition%important component_diff_connected:
   1.216 +proposition component_diff_connected:
   1.217    fixes S :: "'a::metric_space set"
   1.218    assumes "connected S" "connected U" "S \<subseteq> U" and C: "C \<in> components (U - S)"
   1.219    shows "connected(U - C)"
   1.220 -  using%unimportant \<open>connected S\<close> unfolding connected_closedin_eq not_ex de_Morgan_conj
   1.221 +  using \<open>connected S\<close> unfolding connected_closedin_eq not_ex de_Morgan_conj
   1.222  proof clarify
   1.223    fix H3 H4 
   1.224    assume clo3: "closedin (subtopology euclidean (U - C)) H3" 
   1.225 @@ -5175,11 +5175,11 @@
   1.226      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)
   1.227  qed
   1.228  
   1.229 -proposition%important tendsto_componentwise_iff:
   1.230 +proposition tendsto_componentwise_iff:
   1.231    fixes f :: "_ \<Rightarrow> 'b::euclidean_space"
   1.232    shows "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>i \<in> Basis. ((\<lambda>x. (f x \<bullet> i)) \<longlongrightarrow> (l \<bullet> i)) F)"
   1.233           (is "?lhs = ?rhs")
   1.234 -proof%unimportant
   1.235 +proof
   1.236    assume ?lhs
   1.237    then show ?rhs
   1.238      unfolding tendsto_def
     2.1 --- a/src/HOL/Analysis/Continuous_Extension.thy	Mon Jul 09 21:55:40 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Continuous_Extension.thy	Tue Jul 10 09:38:35 2018 +0200
     2.3 @@ -13,7 +13,7 @@
     2.4  text\<open>A difference from HOL Light: all summations over infinite sets equal zero,
     2.5     so the "support" must be made explicit in the summation below!\<close>
     2.6  
     2.7 -proposition%important subordinate_partition_of_unity:
     2.8 +proposition subordinate_partition_of_unity:
     2.9    fixes S :: "'a :: euclidean_space set"
    2.10    assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
    2.11        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> {}}"
    2.12 @@ -22,7 +22,7 @@
    2.13        and "\<And>x U. \<lbrakk>U \<in> \<C>; x \<in> S; x \<notin> U\<rbrakk> \<Longrightarrow> F U x = 0"
    2.14        and "\<And>x. x \<in> S \<Longrightarrow> supp_sum (\<lambda>W. F W x) \<C> = 1"
    2.15        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}"
    2.16 -proof%unimportant (cases "\<exists>W. W \<in> \<C> \<and> S \<subseteq> W")
    2.17 +proof (cases "\<exists>W. W \<in> \<C> \<and> S \<subseteq> W")
    2.18    case True
    2.19      then obtain W where "W \<in> \<C>" "S \<subseteq> W" by metis
    2.20      then show ?thesis
    2.21 @@ -283,7 +283,7 @@
    2.22            "\<And>x. f x = b \<longleftrightarrow> x \<in> T"
    2.23  using assms by (auto intro: Urysohn_local_strong [of UNIV S T])
    2.24  
    2.25 -proposition%important Urysohn:
    2.26 +proposition Urysohn:
    2.27    assumes US: "closed S"
    2.28        and UT: "closed T"
    2.29        and "S \<inter> T = {}"
    2.30 @@ -292,7 +292,7 @@
    2.31            "\<And>x. f x \<in> closed_segment a b"
    2.32            "\<And>x. x \<in> S \<Longrightarrow> f x = a"
    2.33            "\<And>x. x \<in> T \<Longrightarrow> f x = b"
    2.34 -using%unimportant assms by (auto intro: Urysohn_local [of UNIV S T a b])
    2.35 +  using assms by (auto intro: Urysohn_local [of UNIV S T a b])
    2.36  
    2.37  
    2.38  subsection\<open>The Dugundji extension theorem and Tietze variants as corollaries\<close>
    2.39 @@ -300,14 +300,14 @@
    2.40  text%important\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367.
    2.41  https://projecteuclid.org/euclid.pjm/1103052106\<close>
    2.42  
    2.43 -theorem%important Dugundji:
    2.44 +theorem Dugundji:
    2.45    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
    2.46    assumes "convex C" "C \<noteq> {}"
    2.47        and cloin: "closedin (subtopology euclidean U) S"
    2.48        and contf: "continuous_on S f" and "f ` S \<subseteq> C"
    2.49    obtains g where "continuous_on U g" "g ` U \<subseteq> C"
    2.50                    "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
    2.51 -proof%unimportant (cases "S = {}")
    2.52 +proof (cases "S = {}")
    2.53    case True then show thesis
    2.54      apply (rule_tac g="\<lambda>x. SOME y. y \<in> C" in that)
    2.55        apply (rule continuous_intros)
    2.56 @@ -475,7 +475,7 @@
    2.57  qed
    2.58  
    2.59  
    2.60 -corollary%important Tietze:
    2.61 +corollary Tietze:
    2.62    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
    2.63    assumes "continuous_on S f"
    2.64        and "closedin (subtopology euclidean U) S"
    2.65 @@ -483,7 +483,7 @@
    2.66        and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> B"
    2.67    obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
    2.68                    "\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> B"
    2.69 -using%unimportant assms
    2.70 +  using assms
    2.71  by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f])
    2.72  
    2.73  corollary Tietze_closed_interval:
     3.1 --- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Mon Jul 09 21:55:40 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Tue Jul 10 09:38:35 2018 +0200
     3.3 @@ -33,8 +33,8 @@
     3.4    Nested Interval Property.
     3.5  \<close>
     3.6  
     3.7 -theorem%important real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
     3.8 -proof%unimportant
     3.9 +theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
    3.10 +proof
    3.11    assume "\<exists>f::nat \<Rightarrow> real. surj f"
    3.12    then obtain f :: "nat \<Rightarrow> real" where "surj f" ..
    3.13  
     4.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Jul 09 21:55:40 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Jul 10 09:38:35 2018 +0200
     4.3 @@ -2005,9 +2005,9 @@
     4.4    shows "c *\<^sub>R x \<in> cone hull S"
     4.5    by (metis assms cone_cone_hull hull_inc mem_cone)
     4.6  
     4.7 -proposition%important cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
     4.8 +proposition cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
     4.9    (is "?lhs = ?rhs")
    4.10 -proof%unimportant -
    4.11 +proof -
    4.12    {
    4.13      fix x
    4.14      assume "x \<in> ?rhs"
    4.15 @@ -2089,7 +2089,7 @@
    4.16     "~ affine_dependent s \<Longrightarrow> ~ affine_dependent(s - t)"
    4.17  by (meson Diff_subset affine_dependent_subset)
    4.18  
    4.19 -proposition%important affine_dependent_explicit:
    4.20 +proposition affine_dependent_explicit:
    4.21    "affine_dependent p \<longleftrightarrow>
    4.22      (\<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)"
    4.23  proof -
    4.24 @@ -2524,7 +2524,7 @@
    4.25  
    4.26  subsubsection%unimportant \<open>Explicit expression for convex hull\<close>
    4.27  
    4.28 -proposition%important convex_hull_indexed:
    4.29 +proposition convex_hull_indexed:
    4.30    fixes S :: "'a::real_vector set"
    4.31    shows "convex hull S =
    4.32      {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> S) \<and>
    4.33 @@ -4020,11 +4020,11 @@
    4.34      by (auto simp: convex_hull_explicit)
    4.35  qed
    4.36  
    4.37 -theorem%important caratheodory:
    4.38 +theorem caratheodory:
    4.39    "convex hull p =
    4.40      {x::'a::euclidean_space. \<exists>s. finite s \<and> s \<subseteq> p \<and>
    4.41        card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s}"
    4.42 -proof%unimportant safe
    4.43 +proof safe
    4.44    fix x
    4.45    assume "x \<in> convex hull p"
    4.46    then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1"
    4.47 @@ -5871,10 +5871,10 @@
    4.48      done
    4.49  qed
    4.50  
    4.51 -theorem%important radon:
    4.52 +theorem radon:
    4.53    assumes "affine_dependent c"
    4.54    obtains m p where "m \<subseteq> c" "p \<subseteq> c" "m \<inter> p = {}" "(convex hull m) \<inter> (convex hull p) \<noteq> {}"
    4.55 -proof%unimportant -
    4.56 +proof -
    4.57    from assms[unfolded affine_dependent_explicit]
    4.58    obtain s u where
    4.59        "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"
    4.60 @@ -5965,12 +5965,12 @@
    4.61    qed 
    4.62  qed
    4.63  
    4.64 -theorem%important helly:
    4.65 +theorem helly:
    4.66    fixes f :: "'a::euclidean_space set set"
    4.67    assumes "card f \<ge> DIM('a) + 1" "\<forall>s\<in>f. convex s"
    4.68      and "\<And>t. \<lbrakk>t\<subseteq>f; card t = DIM('a) + 1\<rbrakk> \<Longrightarrow> \<Inter>t \<noteq> {}"
    4.69    shows "\<Inter>f \<noteq> {}"
    4.70 -  apply%unimportant (rule helly_induct)
    4.71 +  apply (rule helly_induct)
    4.72    using assms
    4.73    apply auto
    4.74    done
     5.1 --- a/src/HOL/Analysis/L2_Norm.thy	Mon Jul 09 21:55:40 2018 +0100
     5.2 +++ b/src/HOL/Analysis/L2_Norm.thy	Tue Jul 10 09:38:35 2018 +0200
     5.3 @@ -73,9 +73,9 @@
     5.4    unfolding L2_set_def
     5.5    by (simp add: sum_nonneg sum_nonneg_eq_0_iff)
     5.6  
     5.7 -lemma %important L2_set_triangle_ineq:
     5.8 +proposition L2_set_triangle_ineq:
     5.9    "L2_set (\<lambda>i. f i + g i) A \<le> L2_set f A + L2_set g A"
    5.10 -proof %unimportant (cases "finite A")
    5.11 +proof (cases "finite A")
    5.12    case False
    5.13    thus ?thesis by simp
    5.14  next
     6.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Mon Jul 09 21:55:40 2018 +0100
     6.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Tue Jul 10 09:38:35 2018 +0200
     6.3 @@ -377,11 +377,11 @@
     6.4  subsection \<open>Archimedean properties and useful consequences\<close>
     6.5  
     6.6  text\<open>Bernoulli's inequality\<close>
     6.7 -proposition%important Bernoulli_inequality:
     6.8 +proposition Bernoulli_inequality:
     6.9    fixes x :: real
    6.10    assumes "-1 \<le> x"
    6.11      shows "1 + n * x \<le> (1 + x) ^ n"
    6.12 -proof%unimportant (induct n)
    6.13 +proof (induct n)
    6.14    case 0
    6.15    then show ?case by simp
    6.16  next
     7.1 --- a/src/HOL/Analysis/Measure_Space.thy	Mon Jul 09 21:55:40 2018 +0100
     7.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Tue Jul 10 09:38:35 2018 +0200
     7.3 @@ -1513,7 +1513,7 @@
     7.4    "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"
     7.5    by (auto simp add: null_sets_def emeasure_distr)
     7.6  
     7.7 -lemma%important distr_distr:
     7.8 +proposition distr_distr:
     7.9    "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)"
    7.10    by (auto simp add: emeasure_distr measurable_space
    7.11             intro!: arg_cong[where f="emeasure M"] measure_eqI)
    7.12 @@ -2804,11 +2804,11 @@
    7.13    qed auto
    7.14  qed
    7.15  
    7.16 -lemma%important unsigned_Hahn_decomposition:
    7.17 +proposition unsigned_Hahn_decomposition:
    7.18    assumes [simp]: "sets N = sets M" and [measurable]: "A \<in> sets M"
    7.19      and [simp]: "emeasure M A \<noteq> top" "emeasure N A \<noteq> top"
    7.20    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)"
    7.21 -proof%unimportant -
    7.22 +proof -
    7.23    have "\<exists>Y\<in>sets (restrict_space M A).
    7.24      (\<forall>X\<in>sets (restrict_space M A). X \<subseteq> Y \<longrightarrow> (restrict_space N A) X \<le> (restrict_space M A) X) \<and>
    7.25      (\<forall>X\<in>sets (restrict_space M A). X \<inter> Y = {} \<longrightarrow> (restrict_space M A) X \<le> (restrict_space N A) X)"
    7.26 @@ -2867,8 +2867,8 @@
    7.27  
    7.28  end
    7.29  
    7.30 -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)"
    7.31 -  apply%unimportant -
    7.32 +proposition le_measure: "sets M = sets N \<Longrightarrow> M \<le> N \<longleftrightarrow> (\<forall>A\<in>sets M. emeasure M A \<le> emeasure N A)"
    7.33 +  apply -
    7.34    apply (auto simp: le_measure_iff le_fun_def dest: sets_eq_imp_space_eq)
    7.35    subgoal for X
    7.36      by (cases "X \<in> sets M") (auto simp: emeasure_notin_sets)
     8.1 --- a/src/HOL/Analysis/Norm_Arith.thy	Mon Jul 09 21:55:40 2018 +0100
     8.2 +++ b/src/HOL/Analysis/Norm_Arith.thy	Tue Jul 10 09:38:35 2018 +0200
     8.3 @@ -138,7 +138,7 @@
     8.4  
     8.5  text \<open>Hence more metric properties.\<close>
     8.6  
     8.7 -lemma%important dist_triangle_add:
     8.8 +proposition dist_triangle_add:
     8.9    fixes x y x' y' :: "'a::real_normed_vector"
    8.10    shows "dist (x + y) (x' + y') \<le> dist x x' + dist y y'"
    8.11    by norm
     9.1 --- a/src/HOL/Analysis/Path_Connected.thy	Mon Jul 09 21:55:40 2018 +0100
     9.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Tue Jul 10 09:38:35 2018 +0200
     9.3 @@ -1964,11 +1964,11 @@
     9.4    "2 \<le> DIM('N::euclidean_space) \<Longrightarrow> connected(- {a::'N})"
     9.5    by (simp add: path_connected_punctured_universe path_connected_imp_connected)
     9.6  
     9.7 -lemma%important path_connected_sphere:
     9.8 +proposition path_connected_sphere:
     9.9    fixes a :: "'a :: euclidean_space"
    9.10    assumes "2 \<le> DIM('a)"
    9.11    shows "path_connected(sphere a r)"
    9.12 -proof%unimportant (cases r "0::real" rule: linorder_cases)
    9.13 +proof (cases r "0::real" rule: linorder_cases)
    9.14    case less
    9.15    then show ?thesis
    9.16      by (simp add: path_connected_empty)
    9.17 @@ -2289,23 +2289,23 @@
    9.18      using path_connected_translation by metis
    9.19  qed
    9.20  
    9.21 -lemma%important path_connected_annulus:
    9.22 +proposition path_connected_annulus:
    9.23    fixes a :: "'N::euclidean_space"
    9.24    assumes "2 \<le> DIM('N)"
    9.25    shows "path_connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
    9.26          "path_connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
    9.27          "path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
    9.28          "path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> r2}"
    9.29 -  by%unimportant (auto simp: is_interval_def intro!: is_interval_convex convex_imp_path_connected path_connected_2DIM_I [OF assms])
    9.30 -
    9.31 -lemma%important connected_annulus:
    9.32 +  by (auto simp: is_interval_def intro!: is_interval_convex convex_imp_path_connected path_connected_2DIM_I [OF assms])
    9.33 +
    9.34 +proposition connected_annulus:
    9.35    fixes a :: "'N::euclidean_space"
    9.36    assumes "2 \<le> DIM('N::euclidean_space)"
    9.37    shows "connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
    9.38          "connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
    9.39          "connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
    9.40          "connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> r2}"
    9.41 -  by%unimportant (auto simp: path_connected_annulus [OF assms] path_connected_imp_connected)
    9.42 +  by (auto simp: path_connected_annulus [OF assms] path_connected_imp_connected)
    9.43  
    9.44  
    9.45  subsection%unimportant\<open>Relations between components and path components\<close>
    9.46 @@ -3302,14 +3302,14 @@
    9.47  
    9.48  subsection\<open>Condition for an open map's image to contain a ball\<close>
    9.49  
    9.50 -lemma%important ball_subset_open_map_image:
    9.51 +proposition ball_subset_open_map_image:
    9.52    fixes f :: "'a::heine_borel \<Rightarrow> 'b :: {real_normed_vector,heine_borel}"
    9.53    assumes contf: "continuous_on (closure S) f"
    9.54        and oint: "open (f ` interior S)"
    9.55        and le_no: "\<And>z. z \<in> frontier S \<Longrightarrow> r \<le> norm(f z - f a)"
    9.56        and "bounded S" "a \<in> S" "0 < r"
    9.57      shows "ball (f a) r \<subseteq> f ` S"
    9.58 -proof%unimportant (cases "f ` S = UNIV")
    9.59 +proof (cases "f ` S = UNIV")
    9.60    case True then show ?thesis by simp
    9.61  next
    9.62    case False
    9.63 @@ -3868,26 +3868,26 @@
    9.64  
    9.65  text%important\<open>So taking equivalence classes under homotopy would give the fundamental group\<close>
    9.66  
    9.67 -proposition%important homotopic_paths_rid:
    9.68 +proposition homotopic_paths_rid:
    9.69      "\<lbrakk>path p; path_image p \<subseteq> s\<rbrakk> \<Longrightarrow> homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p)) p"
    9.70 -  apply%unimportant (subst homotopic_paths_sym)
    9.71 +  apply (subst homotopic_paths_sym)
    9.72    apply (rule homotopic_paths_reparametrize [where f = "\<lambda>t. if  t \<le> 1 / 2 then 2 *\<^sub>R t else 1"])
    9.73    apply (simp_all del: le_divide_eq_numeral1)
    9.74    apply (subst split_01)
    9.75    apply (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def)+
    9.76    done
    9.77  
    9.78 -proposition%important homotopic_paths_lid:
    9.79 +proposition homotopic_paths_lid:
    9.80     "\<lbrakk>path p; path_image p \<subseteq> s\<rbrakk> \<Longrightarrow> homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p) p"
    9.81 -using%unimportant homotopic_paths_rid [of "reversepath p" s]
    9.82 +  using homotopic_paths_rid [of "reversepath p" s]
    9.83    by (metis homotopic_paths_reversepath path_image_reversepath path_reversepath pathfinish_linepath
    9.84          pathfinish_reversepath reversepath_joinpaths reversepath_linepath)
    9.85  
    9.86 -proposition%important homotopic_paths_assoc:
    9.87 +proposition homotopic_paths_assoc:
    9.88     "\<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;
    9.89       pathfinish q = pathstart r\<rbrakk>
    9.90      \<Longrightarrow> homotopic_paths s (p +++ (q +++ r)) ((p +++ q) +++ r)"
    9.91 -  apply%unimportant (subst homotopic_paths_sym)
    9.92 +  apply (subst homotopic_paths_sym)
    9.93    apply (rule homotopic_paths_reparametrize
    9.94             [where f = "\<lambda>t. if  t \<le> 1 / 2 then inverse 2 *\<^sub>R t
    9.95                             else if  t \<le> 3 / 4 then t - (1 / 4)
    9.96 @@ -3898,10 +3898,10 @@
    9.97    apply (auto simp: joinpaths_def)
    9.98    done
    9.99  
   9.100 -proposition%important homotopic_paths_rinv:
   9.101 +proposition homotopic_paths_rinv:
   9.102    assumes "path p" "path_image p \<subseteq> s"
   9.103      shows "homotopic_paths s (p +++ reversepath p) (linepath (pathstart p) (pathstart p))"
   9.104 -proof%unimportant -
   9.105 +proof -
   9.106    have "continuous_on ({0..1} \<times> {0..1}) (\<lambda>x. (subpath 0 (fst x) p +++ reversepath (subpath 0 (fst x) p)) (snd x))"
   9.107      using assms
   9.108      apply (simp add: joinpaths_def subpath_def reversepath_def path_def del: le_divide_eq_numeral1)
   9.109 @@ -3921,10 +3921,10 @@
   9.110      done
   9.111  qed
   9.112  
   9.113 -proposition%important homotopic_paths_linv:
   9.114 +proposition homotopic_paths_linv:
   9.115    assumes "path p" "path_image p \<subseteq> s"
   9.116      shows "homotopic_paths s (reversepath p +++ p) (linepath (pathfinish p) (pathfinish p))"
   9.117 -using%unimportant homotopic_paths_rinv [of "reversepath p" s] assms by simp
   9.118 +  using homotopic_paths_rinv [of "reversepath p" s] assms by simp
   9.119  
   9.120  
   9.121  subsection\<open>Homotopy of loops without requiring preservation of endpoints\<close>
   9.122 @@ -3994,14 +3994,14 @@
   9.123  
   9.124  subsection\<open>Relations between the two variants of homotopy\<close>
   9.125  
   9.126 -proposition%important homotopic_paths_imp_homotopic_loops:
   9.127 +proposition homotopic_paths_imp_homotopic_loops:
   9.128      "\<lbrakk>homotopic_paths s p q; pathfinish p = pathstart p; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> homotopic_loops s p q"
   9.129 -  by%unimportant (auto simp: homotopic_paths_def homotopic_loops_def intro: homotopic_with_mono)
   9.130 -
   9.131 -proposition%important homotopic_loops_imp_homotopic_paths_null:
   9.132 +  by (auto simp: homotopic_paths_def homotopic_loops_def intro: homotopic_with_mono)
   9.133 +
   9.134 +proposition homotopic_loops_imp_homotopic_paths_null:
   9.135    assumes "homotopic_loops s p (linepath a a)"
   9.136      shows "homotopic_paths s p (linepath (pathstart p) (pathstart p))"
   9.137 -proof%unimportant -
   9.138 +proof -
   9.139    have "path p" by (metis assms homotopic_loops_imp_path)
   9.140    have ploop: "pathfinish p = pathstart p" by (metis assms homotopic_loops_imp_loop)
   9.141    have pip: "path_image p \<subseteq> s" by (metis assms homotopic_loops_imp_subset)
   9.142 @@ -4069,12 +4069,12 @@
   9.143      by (blast intro: homotopic_paths_trans)
   9.144  qed
   9.145  
   9.146 -proposition%important homotopic_loops_conjugate:
   9.147 +proposition homotopic_loops_conjugate:
   9.148    fixes s :: "'a::real_normed_vector set"
   9.149    assumes "path p" "path q" and pip: "path_image p \<subseteq> s" and piq: "path_image q \<subseteq> s"
   9.150        and papp: "pathfinish p = pathstart q" and qloop: "pathfinish q = pathstart q"
   9.151      shows "homotopic_loops s (p +++ q +++ reversepath p) q"
   9.152 -proof%unimportant -
   9.153 +proof -
   9.154    have contp: "continuous_on {0..1} p"  using \<open>path p\<close> [unfolded path_def] by blast
   9.155    have contq: "continuous_on {0..1} q"  using \<open>path q\<close> [unfolded path_def] by blast
   9.156    have c1: "continuous_on ({0..1} \<times> {0..1}) (\<lambda>x. p ((1 - fst x) * snd x + fst x))"
   9.157 @@ -4326,10 +4326,10 @@
   9.158      using homotopic_join_subpaths2 by blast
   9.159  qed
   9.160  
   9.161 -proposition%important homotopic_join_subpaths:
   9.162 +proposition homotopic_join_subpaths:
   9.163     "\<lbrakk>path g; path_image g \<subseteq> s; u \<in> {0..1}; v \<in> {0..1}; w \<in> {0..1}\<rbrakk>
   9.164      \<Longrightarrow> homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
   9.165 -apply%unimportant (rule le_cases3 [of u v w])
   9.166 +  apply (rule le_cases3 [of u v w])
   9.167  using homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3 by metis+
   9.168  
   9.169  text\<open>Relating homotopy of trivial loops to path-connectedness.\<close>
   9.170 @@ -5043,7 +5043,7 @@
   9.171  
   9.172  subsection\<open>Sort of induction principle for connected sets\<close>
   9.173  
   9.174 -lemma%important connected_induction:
   9.175 +proposition connected_induction:
   9.176    assumes "connected S"
   9.177        and opD: "\<And>T a. \<lbrakk>openin (subtopology euclidean S) T; a \<in> T\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> T \<and> P z"
   9.178        and opI: "\<And>a. a \<in> S
   9.179 @@ -5051,7 +5051,7 @@
   9.180                       (\<forall>x \<in> T. \<forall>y \<in> T. P x \<and> P y \<and> Q x \<longrightarrow> Q y)"
   9.181        and etc: "a \<in> S" "b \<in> S" "P a" "P b" "Q a"
   9.182      shows "Q b"
   9.183 -proof%unimportant -
   9.184 +proof -
   9.185    have 1: "openin (subtopology euclidean S)
   9.186               {b. \<exists>T. openin (subtopology euclidean S) T \<and>
   9.187                       b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> Q x)}"
   9.188 @@ -5142,14 +5142,14 @@
   9.189  
   9.190  subsection\<open>Basic properties of local compactness\<close>
   9.191  
   9.192 -lemma%important locally_compact:
   9.193 +proposition locally_compact:
   9.194    fixes s :: "'a :: metric_space set"
   9.195    shows
   9.196      "locally compact s \<longleftrightarrow>
   9.197       (\<forall>x \<in> s. \<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and>
   9.198                      openin (subtopology euclidean s) u \<and> compact v)"
   9.199       (is "?lhs = ?rhs")
   9.200 -proof%unimportant
   9.201 +proof
   9.202    assume ?lhs
   9.203    then show ?rhs
   9.204      apply clarify
   9.205 @@ -5696,12 +5696,12 @@
   9.206      by (metis \<open>U = S \<inter> V\<close> inf.bounded_iff openin_imp_subset that)
   9.207  qed
   9.208  
   9.209 -corollary%important Sura_Bura:
   9.210 +corollary Sura_Bura:
   9.211    fixes S :: "'a::euclidean_space set"
   9.212    assumes "locally compact S" "C \<in> components S" "compact C"
   9.213    shows "C = \<Inter> {K. C \<subseteq> K \<and> compact K \<and> openin (subtopology euclidean S) K}"
   9.214           (is "C = ?rhs")
   9.215 -proof%unimportant
   9.216 +proof
   9.217    show "?rhs \<subseteq> C"
   9.218    proof (clarsimp, rule ccontr)
   9.219      fix x
   9.220 @@ -5831,17 +5831,17 @@
   9.221      by (metis assms(1) assms(2) assms(3) mem_Collect_eq path_component_subset path_connected_path_component)
   9.222  qed
   9.223  
   9.224 -proposition%important locally_path_connected:
   9.225 +proposition locally_path_connected:
   9.226    "locally path_connected S \<longleftrightarrow>
   9.227     (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
   9.228            \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v))"
   9.229 -by%unimportant (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
   9.230 -
   9.231 -proposition%important locally_path_connected_open_path_component:
   9.232 +  by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
   9.233 +
   9.234 +proposition locally_path_connected_open_path_component:
   9.235    "locally path_connected S \<longleftrightarrow>
   9.236     (\<forall>t x. openin (subtopology euclidean S) t \<and> x \<in> t
   9.237            \<longrightarrow> openin (subtopology euclidean S) (path_component_set t x))"
   9.238 -by%unimportant (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
   9.239 +  by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
   9.240  
   9.241  lemma locally_connected_open_component:
   9.242    "locally connected S \<longleftrightarrow>
   9.243 @@ -5849,14 +5849,14 @@
   9.244            \<longrightarrow> openin (subtopology euclidean S) c)"
   9.245  by (metis components_iff locally_connected_open_connected_component)
   9.246  
   9.247 -proposition%important locally_connected_im_kleinen:
   9.248 +proposition locally_connected_im_kleinen:
   9.249    "locally connected S \<longleftrightarrow>
   9.250     (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
   9.251         \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and>
   9.252                  x \<in> u \<and> u \<subseteq> v \<and>
   9.253                  (\<forall>y. y \<in> u \<longrightarrow> (\<exists>c. connected c \<and> c \<subseteq> v \<and> x \<in> c \<and> y \<in> c))))"
   9.254     (is "?lhs = ?rhs")
   9.255 -proof%unimportant
   9.256 +proof
   9.257    assume ?lhs
   9.258    then show ?rhs
   9.259      by (fastforce simp add: locally_connected)
   9.260 @@ -5890,7 +5890,7 @@
   9.261      done
   9.262  qed
   9.263  
   9.264 -proposition%important locally_path_connected_im_kleinen:
   9.265 +proposition locally_path_connected_im_kleinen:
   9.266    "locally path_connected S \<longleftrightarrow>
   9.267     (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
   9.268         \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and>
   9.269 @@ -5898,7 +5898,7 @@
   9.270                  (\<forall>y. y \<in> u \<longrightarrow> (\<exists>p. path p \<and> path_image p \<subseteq> v \<and>
   9.271                                  pathstart p = x \<and> pathfinish p = y))))"
   9.272     (is "?lhs = ?rhs")
   9.273 -proof%unimportant
   9.274 +proof
   9.275    assume ?lhs
   9.276    then show ?rhs
   9.277      apply (simp add: locally_path_connected path_connected_def)
   9.278 @@ -6048,13 +6048,13 @@
   9.279    shows "open S \<Longrightarrow> path_component_set S x = connected_component_set S x"
   9.280  by (simp add: open_path_connected_component)
   9.281  
   9.282 -proposition%important locally_connected_quotient_image:
   9.283 +proposition locally_connected_quotient_image:
   9.284    assumes lcS: "locally connected S"
   9.285        and oo: "\<And>T. T \<subseteq> f ` S
   9.286                  \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow>
   9.287                      openin (subtopology euclidean (f ` S)) T"
   9.288      shows "locally connected (f ` S)"
   9.289 -proof%unimportant (clarsimp simp: locally_connected_open_component)
   9.290 +proof (clarsimp simp: locally_connected_open_component)
   9.291    fix U C
   9.292    assume opefSU: "openin (subtopology euclidean (f ` S)) U" and "C \<in> components U"
   9.293    then have "C \<subseteq> U" "U \<subseteq> f ` S"
   9.294 @@ -6114,12 +6114,12 @@
   9.295  qed
   9.296  
   9.297  text\<open>The proof resembles that above but is not identical!\<close>
   9.298 -proposition%important locally_path_connected_quotient_image:
   9.299 +proposition locally_path_connected_quotient_image:
   9.300    assumes lcS: "locally path_connected S"
   9.301        and oo: "\<And>T. T \<subseteq> f ` S
   9.302                  \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow> openin (subtopology euclidean (f ` S)) T"
   9.303      shows "locally path_connected (f ` S)"
   9.304 -proof%unimportant (clarsimp simp: locally_path_connected_open_path_component)
   9.305 +proof (clarsimp simp: locally_path_connected_open_path_component)
   9.306    fix U y
   9.307    assume opefSU: "openin (subtopology euclidean (f ` S)) U" and "y \<in> U"
   9.308    then have "path_component_set U y \<subseteq> U" "U \<subseteq> f ` S"
   9.309 @@ -6345,7 +6345,7 @@
   9.310      by (rule that [OF \<open>linear f\<close> \<open>f ` S \<subseteq> T\<close>])
   9.311  qed
   9.312  
   9.313 -proposition%important isometries_subspaces:
   9.314 +proposition isometries_subspaces:
   9.315    fixes S :: "'a::euclidean_space set"
   9.316      and T :: "'b::euclidean_space set"
   9.317    assumes S: "subspace S"
   9.318 @@ -6356,7 +6356,7 @@
   9.319                      "\<And>x. x \<in> T \<Longrightarrow> norm(g x) = norm x"
   9.320                      "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
   9.321                      "\<And>x. x \<in> T \<Longrightarrow> f(g x) = x"
   9.322 -proof%unimportant -
   9.323 +proof -
   9.324    obtain B where "B \<subseteq> S" and Borth: "pairwise orthogonal B"
   9.325               and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
   9.326               and "independent B" "finite B" "card B = dim S" "span B = S"
   9.327 @@ -7815,7 +7815,7 @@
   9.328    qed
   9.329  qed
   9.330  
   9.331 -proposition%important homeomorphism_moving_points_exists:
   9.332 +proposition homeomorphism_moving_points_exists:
   9.333    fixes S :: "'a::euclidean_space set"
   9.334    assumes 2: "2 \<le> DIM('a)" "open S" "connected S" "S \<subseteq> T" "finite K"
   9.335        and KS: "\<And>i. i \<in> K \<Longrightarrow> x i \<in> S \<and> y i \<in> S"
   9.336 @@ -7823,7 +7823,7 @@
   9.337        and S: "S \<subseteq> T" "T \<subseteq> affine hull S" "connected S"
   9.338    obtains f g where "homeomorphism T T f g" "\<And>i. i \<in> K \<Longrightarrow> f(x i) = y i"
   9.339                      "{x. ~ (f x = x \<and> g x = x)} \<subseteq> S" "bounded {x. (~ (f x = x \<and> g x = x))}"
   9.340 -proof%unimportant (cases "S = {}")
   9.341 +proof (cases "S = {}")
   9.342    case True
   9.343    then show ?thesis
   9.344      using KS homeomorphism_ident that by fastforce
   9.345 @@ -8082,12 +8082,12 @@
   9.346    qed
   9.347  qed
   9.348  
   9.349 -proposition%important homeomorphism_grouping_points_exists:
   9.350 +proposition homeomorphism_grouping_points_exists:
   9.351    fixes S :: "'a::euclidean_space set"
   9.352    assumes "open U" "open S" "connected S" "U \<noteq> {}" "finite K" "K \<subseteq> S" "U \<subseteq> S" "S \<subseteq> T"
   9.353    obtains f g where "homeomorphism T T f g" "{x. (~ (f x = x \<and> g x = x))} \<subseteq> S"
   9.354                      "bounded {x. (~ (f x = x \<and> g x = x))}" "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U"
   9.355 -proof%unimportant (cases "2 \<le> DIM('a)")
   9.356 +proof (cases "2 \<le> DIM('a)")
   9.357    case True
   9.358    have TS: "T \<subseteq> affine hull S"
   9.359      using affine_hull_open assms by blast
   9.360 @@ -8364,13 +8364,13 @@
   9.361    qed
   9.362  qed
   9.363  
   9.364 -proposition%important nullhomotopic_from_sphere_extension:
   9.365 +proposition nullhomotopic_from_sphere_extension:
   9.366    fixes f :: "'M::euclidean_space \<Rightarrow> 'a::real_normed_vector"
   9.367    shows  "(\<exists>c. homotopic_with (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)) \<longleftrightarrow>
   9.368            (\<exists>g. continuous_on (cball a r) g \<and> g ` (cball a r) \<subseteq> S \<and>
   9.369                 (\<forall>x \<in> sphere a r. g x = f x))"
   9.370           (is "?lhs = ?rhs")
   9.371 -proof%unimportant (cases r "0::real" rule: linorder_cases)
   9.372 +proof (cases r "0::real" rule: linorder_cases)
   9.373    case equal
   9.374    then show ?thesis
   9.375      apply (auto simp: homotopic_with)
    10.1 --- a/src/HOL/Analysis/Product_Vector.thy	Mon Jul 09 21:55:40 2018 +0100
    10.2 +++ b/src/HOL/Analysis/Product_Vector.thy	Tue Jul 10 09:38:35 2018 +0200
    10.3 @@ -314,11 +314,11 @@
    10.4  
    10.5  subsubsection%unimportant \<open>Pair operations are linear\<close>
    10.6  
    10.7 -lemma%important bounded_linear_fst: "bounded_linear fst"
    10.8 +proposition bounded_linear_fst: "bounded_linear fst"
    10.9    using fst_add fst_scaleR
   10.10    by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
   10.11  
   10.12 -lemma%important bounded_linear_snd: "bounded_linear snd"
   10.13 +proposition bounded_linear_snd: "bounded_linear snd"
   10.14    using snd_add snd_scaleR
   10.15    by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
   10.16  
   10.17 @@ -354,10 +354,10 @@
   10.18  
   10.19  subsubsection%unimportant \<open>Frechet derivatives involving pairs\<close>
   10.20  
   10.21 -lemma%important has_derivative_Pair [derivative_intros]:
   10.22 +proposition has_derivative_Pair [derivative_intros]:
   10.23    assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
   10.24    shows "((\<lambda>x. (f x, g x)) has_derivative (\<lambda>h. (f' h, g' h))) (at x within s)"
   10.25 -proof%unimportant (rule has_derivativeI_sandwich[of 1])
   10.26 +proof (rule has_derivativeI_sandwich[of 1])
   10.27    show "bounded_linear (\<lambda>h. (f' h, g' h))"
   10.28      using f g by (intro bounded_linear_Pair has_derivative_bounded_linear)
   10.29    let ?Rf = "\<lambda>y. f y - f x - f' (y - x)"
    11.1 --- a/src/HOL/Analysis/Sigma_Algebra.thy	Mon Jul 09 21:55:40 2018 +0100
    11.2 +++ b/src/HOL/Analysis/Sigma_Algebra.thy	Tue Jul 10 09:38:35 2018 +0200
    11.3 @@ -146,13 +146,13 @@
    11.4    "a \<in> M \<Longrightarrow> \<Omega> - a \<in> M"
    11.5    by auto
    11.6  
    11.7 -lemma%important algebra_iff_Un:
    11.8 +proposition algebra_iff_Un:
    11.9    "algebra \<Omega> M \<longleftrightarrow>
   11.10      M \<subseteq> Pow \<Omega> \<and>
   11.11      {} \<in> M \<and>
   11.12      (\<forall>a \<in> M. \<Omega> - a \<in> M) \<and>
   11.13      (\<forall>a \<in> M. \<forall> b \<in> M. a \<union> b \<in> M)" (is "_ \<longleftrightarrow> ?Un")
   11.14 -proof%unimportant
   11.15 +proof
   11.16    assume "algebra \<Omega> M"
   11.17    then interpret algebra \<Omega> M .
   11.18    show ?Un using sets_into_space by auto
   11.19 @@ -173,12 +173,12 @@
   11.20    show "algebra \<Omega> M" proof qed fact
   11.21  qed
   11.22  
   11.23 -lemma%important algebra_iff_Int:
   11.24 +proposition algebra_iff_Int:
   11.25       "algebra \<Omega> M \<longleftrightarrow>
   11.26         M \<subseteq> Pow \<Omega> & {} \<in> M &
   11.27         (\<forall>a \<in> M. \<Omega> - a \<in> M) &
   11.28         (\<forall>a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)" (is "_ \<longleftrightarrow> ?Int")
   11.29 -proof%unimportant
   11.30 +proof
   11.31    assume "algebra \<Omega> M"
   11.32    then interpret algebra \<Omega> M .
   11.33    show ?Int using sets_into_space by auto
   11.34 @@ -1433,7 +1433,7 @@
   11.35  text%important \<open>The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras
   11.36  generated by a generator closed under intersection.\<close>
   11.37  
   11.38 -lemma%important sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
   11.39 +proposition sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
   11.40    assumes "Int_stable G"
   11.41      and closed: "G \<subseteq> Pow \<Omega>"
   11.42      and A: "A \<in> sigma_sets \<Omega> G"
   11.43 @@ -1442,7 +1442,7 @@
   11.44      and compl: "\<And>A. A \<in> sigma_sets \<Omega> G \<Longrightarrow> P A \<Longrightarrow> P (\<Omega> - A)"
   11.45      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)"
   11.46    shows "P A"
   11.47 -proof%unimportant -
   11.48 +proof -
   11.49    let ?D = "{ A \<in> sigma_sets \<Omega> G. P A }"
   11.50    interpret sigma_algebra \<Omega> "sigma_sets \<Omega> G"
   11.51      using closed by (rule sigma_algebra_sigma_sets)
   11.52 @@ -1633,12 +1633,12 @@
   11.53  
   11.54  subsubsection \<open>Constructing simple @{typ "'a measure"}\<close>
   11.55  
   11.56 -lemma%important emeasure_measure_of:
   11.57 +proposition emeasure_measure_of:
   11.58    assumes M: "M = measure_of \<Omega> A \<mu>"
   11.59    assumes ms: "A \<subseteq> Pow \<Omega>" "positive (sets M) \<mu>" "countably_additive (sets M) \<mu>"
   11.60    assumes X: "X \<in> sets M"
   11.61    shows "emeasure M X = \<mu> X"
   11.62 -proof%unimportant -
   11.63 +proof -
   11.64    interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" by (rule sigma_algebra_sigma_sets) fact
   11.65    have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>"
   11.66      using ms M by (simp add: measure_space_def sigma_algebra_sigma_sets)
    12.1 --- a/src/HOL/Analysis/Starlike.thy	Mon Jul 09 21:55:40 2018 +0100
    12.2 +++ b/src/HOL/Analysis/Starlike.thy	Tue Jul 10 09:38:35 2018 +0200
    12.3 @@ -5063,12 +5063,12 @@
    12.4  
    12.5  subsection\<open>Connectedness of the intersection of a chain\<close>
    12.6  
    12.7 -proposition%important connected_chain:
    12.8 +proposition connected_chain:
    12.9    fixes \<F> :: "'a :: euclidean_space set set"
   12.10    assumes cc: "\<And>S. S \<in> \<F> \<Longrightarrow> compact S \<and> connected S"
   12.11        and linear: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
   12.12    shows "connected(\<Inter>\<F>)"
   12.13 -proof%unimportant (cases "\<F> = {}")
   12.14 +proof (cases "\<F> = {}")
   12.15    case True then show ?thesis
   12.16      by auto
   12.17  next
   12.18 @@ -5212,13 +5212,13 @@
   12.19        by (meson le_max_iff_disj)
   12.20  qed
   12.21  
   12.22 -proposition%important proper_map:
   12.23 +proposition proper_map:
   12.24    fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
   12.25    assumes "closedin (subtopology euclidean S) K"
   12.26        and com: "\<And>U. \<lbrakk>U \<subseteq> T; compact U\<rbrakk> \<Longrightarrow> compact (S \<inter> f -` U)"
   12.27        and "f ` S \<subseteq> T"
   12.28      shows "closedin (subtopology euclidean T) (f ` K)"
   12.29 -proof%unimportant -
   12.30 +proof -
   12.31    have "K \<subseteq> S"
   12.32      using assms closedin_imp_subset by metis
   12.33    obtain C where "closed C" and Keq: "K = S \<inter> C"
   12.34 @@ -6708,11 +6708,11 @@
   12.35    by (metis a orthogonal_clauses(1,2,4)
   12.36        span_induct_alt x)
   12.37  
   12.38 -proposition%important Gram_Schmidt_step:
   12.39 +proposition Gram_Schmidt_step:
   12.40    fixes S :: "'a::euclidean_space set"
   12.41    assumes S: "pairwise orthogonal S" and x: "x \<in> span S"
   12.42      shows "orthogonal x (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b))"
   12.43 -proof%unimportant -
   12.44 +proof -
   12.45    have "finite S"
   12.46      by (simp add: S pairwise_orthogonal_imp_finite)
   12.47    have "orthogonal (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)) x"
   12.48 @@ -6767,11 +6767,11 @@
   12.49  qed
   12.50  
   12.51  
   12.52 -proposition%important orthogonal_extension:
   12.53 +proposition orthogonal_extension:
   12.54    fixes S :: "'a::euclidean_space set"
   12.55    assumes S: "pairwise orthogonal S"
   12.56    obtains U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
   12.57 -proof%unimportant -
   12.58 +proof -
   12.59    obtain B where "finite B" "span B = span T"
   12.60      using basis_subspace_exists [of "span T"] subspace_span by metis
   12.61    with orthogonal_extension_aux [of B S]
   12.62 @@ -6827,13 +6827,13 @@
   12.63      done
   12.64  qed
   12.65  
   12.66 -proposition%important orthonormal_basis_subspace:
   12.67 +proposition orthonormal_basis_subspace:
   12.68    fixes S :: "'a :: euclidean_space set"
   12.69    assumes "subspace S"
   12.70    obtains B where "B \<subseteq> S" "pairwise orthogonal B"
   12.71                and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
   12.72                and "independent B" "card B = dim S" "span B = S"
   12.73 -proof%unimportant -
   12.74 +proof -
   12.75    obtain B where "0 \<notin> B" "B \<subseteq> S"
   12.76               and orth: "pairwise orthogonal B"
   12.77               and "independent B" "card B = dim S" "span B = S"
   12.78 @@ -6864,11 +6864,11 @@
   12.79  qed
   12.80  
   12.81  
   12.82 -proposition%important orthogonal_to_subspace_exists_gen:
   12.83 +proposition orthogonal_to_subspace_exists_gen:
   12.84    fixes S :: "'a :: euclidean_space set"
   12.85    assumes "span S \<subset> span T"
   12.86    obtains x where "x \<noteq> 0" "x \<in> span T" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
   12.87 -proof%unimportant -
   12.88 +proof -
   12.89    obtain B where "B \<subseteq> span S" and orthB: "pairwise orthogonal B"
   12.90               and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
   12.91               and "independent B" "card B = dim S" "span B = span S"
   12.92 @@ -6933,10 +6933,10 @@
   12.93      by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_base that)
   12.94  qed
   12.95  
   12.96 -proposition%important orthogonal_subspace_decomp_exists:
   12.97 +proposition orthogonal_subspace_decomp_exists:
   12.98    fixes S :: "'a :: euclidean_space set"
   12.99    obtains y z where "y \<in> span S" "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w" "x = y + z"
  12.100 -proof%unimportant -
  12.101 +proof -
  12.102    obtain T where "0 \<notin> T" "T \<subseteq> span S" "pairwise orthogonal T" "independent T"
  12.103      "card T = dim (span S)" "span T = span S"
  12.104      using orthogonal_basis_subspace subspace_span by blast
  12.105 @@ -7030,11 +7030,11 @@
  12.106    qed
  12.107  qed
  12.108  
  12.109 -proposition%important dim_orthogonal_sum:
  12.110 +proposition dim_orthogonal_sum:
  12.111    fixes A :: "'a::euclidean_space set"
  12.112    assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
  12.113      shows "dim(A \<union> B) = dim A + dim B"
  12.114 -proof%unimportant -
  12.115 +proof -
  12.116    have 1: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
  12.117      by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms)
  12.118    have "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
  12.119 @@ -7163,10 +7163,10 @@
  12.120  
  12.121  subsection\<open>Lower-dimensional affine subsets are nowhere dense\<close>
  12.122  
  12.123 -proposition%important dense_complement_subspace:
  12.124 +proposition dense_complement_subspace:
  12.125    fixes S :: "'a :: euclidean_space set"
  12.126    assumes dim_less: "dim T < dim S" and "subspace S" shows "closure(S - T) = S"
  12.127 -proof%unimportant -
  12.128 +proof -
  12.129    have "closure(S - U) = S" if "dim U < dim S" "U \<subseteq> S" for U
  12.130    proof -
  12.131      have "span U \<subset> span S"
  12.132 @@ -7465,7 +7465,7 @@
  12.133  
  12.134  subsection\<open>Several Variants of Paracompactness\<close>
  12.135  
  12.136 -proposition%important paracompact:
  12.137 +proposition paracompact:
  12.138    fixes S :: "'a :: euclidean_space set"
  12.139    assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
  12.140    obtains \<C>' where "S \<subseteq> \<Union> \<C>'"
  12.141 @@ -7473,7 +7473,7 @@
  12.142                 and "\<And>x. x \<in> S
  12.143                         \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and>
  12.144                                 finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
  12.145 -proof%unimportant (cases "S = {}")
  12.146 +proof (cases "S = {}")
  12.147    case True with that show ?thesis by blast
  12.148  next
  12.149    case False
  12.150 @@ -7858,14 +7858,14 @@
  12.151  
  12.152  subsection\<open>Covering an open set by a countable chain of compact sets\<close>
  12.153    
  12.154 -proposition%important open_Union_compact_subsets:
  12.155 +proposition open_Union_compact_subsets:
  12.156    fixes S :: "'a::euclidean_space set"
  12.157    assumes "open S"
  12.158    obtains C where "\<And>n. compact(C n)" "\<And>n. C n \<subseteq> S"
  12.159                    "\<And>n. C n \<subseteq> interior(C(Suc n))"
  12.160                    "\<Union>(range C) = S"
  12.161                    "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. K \<subseteq> (C n)"
  12.162 -proof%unimportant (cases "S = {}")
  12.163 +proof (cases "S = {}")
  12.164    case True
  12.165    then show ?thesis
  12.166      by (rule_tac C = "\<lambda>n. {}" in that) auto
    13.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Jul 09 21:55:40 2018 +0100
    13.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Jul 10 09:38:35 2018 +0200
    13.3 @@ -640,7 +640,7 @@
    13.4  
    13.5  subsubsection \<open>Main properties of open sets\<close>
    13.6  
    13.7 -lemma%important openin_clauses:
    13.8 +proposition openin_clauses:
    13.9    fixes U :: "'a topology"
   13.10    shows
   13.11      "openin U {}"
   13.12 @@ -2765,16 +2765,16 @@
   13.13  
   13.14  subsection \<open>Limits\<close>
   13.15  
   13.16 -lemma%important Lim: "(f \<longlongrightarrow> l) net \<longleftrightarrow> trivial_limit net \<or> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
   13.17 +proposition Lim: "(f \<longlongrightarrow> l) net \<longleftrightarrow> trivial_limit net \<or> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
   13.18    by (auto simp: tendsto_iff trivial_limit_eq)
   13.19  
   13.20  text \<open>Show that they yield usual definitions in the various cases.\<close>
   13.21  
   13.22 -lemma%important Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
   13.23 +proposition Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
   13.24      (\<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)"
   13.25    by (auto simp: tendsto_iff eventually_at_le)
   13.26  
   13.27 -lemma%important Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
   13.28 +proposition Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
   13.29      (\<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)"
   13.30    by (auto simp: tendsto_iff eventually_at)
   13.31  
   13.32 @@ -2785,11 +2785,11 @@
   13.33    apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
   13.34    done
   13.35  
   13.36 -lemma%important Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
   13.37 +proposition Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
   13.38      (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d  \<longrightarrow> dist (f x) l < e)"
   13.39    by (auto simp: tendsto_iff eventually_at)
   13.40  
   13.41 -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)"
   13.42 +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)"
   13.43    by (auto simp: tendsto_iff eventually_at_infinity)
   13.44  
   13.45  corollary Lim_at_infinityI [intro?]:
   13.46 @@ -3652,12 +3652,12 @@
   13.47  
   13.48  subsubsection \<open>Bolzano-Weierstrass property\<close>
   13.49  
   13.50 -lemma%important heine_borel_imp_bolzano_weierstrass:
   13.51 +proposition heine_borel_imp_bolzano_weierstrass:
   13.52    assumes "compact s"
   13.53      and "infinite t"
   13.54      and "t \<subseteq> s"
   13.55    shows "\<exists>x \<in> s. x islimpt t"
   13.56 -proof%unimportant (rule ccontr)
   13.57 +proof (rule ccontr)
   13.58    assume "\<not> (\<exists>x \<in> s. x islimpt t)"
   13.59    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)"
   13.60      unfolding islimpt_def
   13.61 @@ -4170,9 +4170,9 @@
   13.62      unfolding C_def by (intro exI[of _ "f`T"]) fastforce
   13.63  qed
   13.64  
   13.65 -lemma%important countably_compact_imp_compact_second_countable:
   13.66 +proposition countably_compact_imp_compact_second_countable:
   13.67    "countably_compact U \<Longrightarrow> compact (U :: 'a :: second_countable_topology set)"
   13.68 -proof%unimportant (rule countably_compact_imp_compact)
   13.69 +proof (rule countably_compact_imp_compact)
   13.70    fix T and x :: 'a
   13.71    assume "open T" "x \<in> T"
   13.72    from topological_basisE[OF is_basis this] obtain b where
   13.73 @@ -4448,10 +4448,10 @@
   13.74    shows "seq_compact U \<longleftrightarrow> compact U"
   13.75    using seq_compact_eq_countably_compact countably_compact_eq_compact by blast
   13.76  
   13.77 -lemma%important bolzano_weierstrass_imp_seq_compact:
   13.78 +proposition bolzano_weierstrass_imp_seq_compact:
   13.79    fixes s :: "'a::{t1_space, first_countable_topology} set"
   13.80    shows "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> seq_compact s"
   13.81 -  by%unimportant (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
   13.82 +  by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
   13.83  
   13.84  
   13.85  subsubsection\<open>Totally bounded\<close>
   13.86 @@ -4459,10 +4459,10 @@
   13.87  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)"
   13.88    unfolding Cauchy_def by metis
   13.89  
   13.90 -lemma%important seq_compact_imp_totally_bounded:
   13.91 +proposition seq_compact_imp_totally_bounded:
   13.92    assumes "seq_compact s"
   13.93    shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>k. ball x e)"
   13.94 -proof%unimportant -
   13.95 +proof -
   13.96    { 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)"
   13.97      let ?Q = "\<lambda>x n r. r \<in> s \<and> (\<forall>m < (n::nat). \<not> (dist (x m) r < e))"
   13.98      have "\<exists>x. \<forall>n::nat. ?Q x n (x n)"
   13.99 @@ -4491,11 +4491,11 @@
  13.100  
  13.101  subsubsection\<open>Heine-Borel theorem\<close>
  13.102  
  13.103 -lemma%important seq_compact_imp_heine_borel:
  13.104 +proposition seq_compact_imp_heine_borel:
  13.105    fixes s :: "'a :: metric_space set"
  13.106    assumes "seq_compact s"
  13.107    shows "compact s"
  13.108 -proof%unimportant -
  13.109 +proof -
  13.110    from seq_compact_imp_totally_bounded[OF \<open>seq_compact s\<close>]
  13.111    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)"
  13.112      unfolding choice_iff' ..
  13.113 @@ -4536,22 +4536,22 @@
  13.114    qed
  13.115  qed
  13.116  
  13.117 -lemma%important compact_eq_seq_compact_metric:
  13.118 +proposition compact_eq_seq_compact_metric:
  13.119    "compact (s :: 'a::metric_space set) \<longleftrightarrow> seq_compact s"
  13.120    using compact_imp_seq_compact seq_compact_imp_heine_borel by blast
  13.121  
  13.122 -lemma%important compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
  13.123 +proposition compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
  13.124    "compact (S :: 'a::metric_space set) \<longleftrightarrow>
  13.125     (\<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))"
  13.126    unfolding compact_eq_seq_compact_metric seq_compact_def by auto
  13.127  
  13.128  subsubsection \<open>Complete the chain of compactness variants\<close>
  13.129  
  13.130 -lemma%important compact_eq_bolzano_weierstrass:
  13.131 +proposition compact_eq_bolzano_weierstrass:
  13.132    fixes s :: "'a::metric_space set"
  13.133    shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))"
  13.134    (is "?lhs = ?rhs")
  13.135 -proof%unimportant
  13.136 +proof
  13.137    assume ?lhs
  13.138    then show ?rhs
  13.139      using heine_borel_imp_bolzano_weierstrass[of s] by auto
  13.140 @@ -4561,7 +4561,7 @@
  13.141      unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact)
  13.142  qed
  13.143  
  13.144 -lemma%important bolzano_weierstrass_imp_bounded:
  13.145 +proposition bolzano_weierstrass_imp_bounded:
  13.146    "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s"
  13.147    using compact_imp_bounded unfolding compact_eq_bolzano_weierstrass .
  13.148  
  13.149 @@ -4577,12 +4577,12 @@
  13.150    assumes bounded_imp_convergent_subsequence:
  13.151      "bounded (range f) \<Longrightarrow> \<exists>l r. strict_mono (r::nat\<Rightarrow>nat) \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
  13.152  
  13.153 -lemma%important bounded_closed_imp_seq_compact:
  13.154 +proposition bounded_closed_imp_seq_compact:
  13.155    fixes s::"'a::heine_borel set"
  13.156    assumes "bounded s"
  13.157      and "closed s"
  13.158    shows "seq_compact s"
  13.159 -proof%unimportant (unfold seq_compact_def, clarify)
  13.160 +proof (unfold seq_compact_def, clarify)
  13.161    fix f :: "nat \<Rightarrow> 'a"
  13.162    assume f: "\<forall>n. f n \<in> s"
  13.163    with \<open>bounded s\<close> have "bounded (range f)"
  13.164 @@ -4807,12 +4807,12 @@
  13.165  
  13.166  subsubsection \<open>Completeness\<close>
  13.167  
  13.168 -lemma%important (in metric_space) completeI:
  13.169 +proposition (in metric_space) completeI:
  13.170    assumes "\<And>f. \<forall>n. f n \<in> s \<Longrightarrow> Cauchy f \<Longrightarrow> \<exists>l\<in>s. f \<longlonglongrightarrow> l"
  13.171    shows "complete s"
  13.172    using assms unfolding complete_def by fast
  13.173  
  13.174 -lemma%important (in metric_space) completeE:
  13.175 +proposition (in metric_space) completeE:
  13.176    assumes "complete s" and "\<forall>n. f n \<in> s" and "Cauchy f"
  13.177    obtains l where "l \<in> s" and "f \<longlonglongrightarrow> l"
  13.178    using assms unfolding complete_def by fast
  13.179 @@ -4862,10 +4862,10 @@
  13.180    then show ?thesis unfolding complete_def by auto
  13.181  qed
  13.182  
  13.183 -lemma%important compact_eq_totally_bounded:
  13.184 +proposition compact_eq_totally_bounded:
  13.185    "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))"
  13.186      (is "_ \<longleftrightarrow> ?rhs")
  13.187 -proof%unimportant
  13.188 +proof
  13.189    assume assms: "?rhs"
  13.190    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)"
  13.191      by (auto simp: choice_iff')
  13.192 @@ -5069,7 +5069,7 @@
  13.193  
  13.194  text\<open>Derive the epsilon-delta forms, which we often use as "definitions"\<close>
  13.195  
  13.196 -lemma%important continuous_within_eps_delta:
  13.197 +proposition continuous_within_eps_delta:
  13.198    "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)"
  13.199    unfolding continuous_within and Lim_within  by fastforce
  13.200  
    14.1 --- a/src/HOL/ROOT	Mon Jul 09 21:55:40 2018 +0100
    14.2 +++ b/src/HOL/ROOT	Tue Jul 10 09:38:35 2018 +0200
    14.3 @@ -58,7 +58,7 @@
    14.4    document_files "root.bib" "root.tex"
    14.5  
    14.6  session "HOL-Analysis" (main timing) in Analysis = HOL +
    14.7 -  options [document_tags = "%unimportant",
    14.8 +  options [document_tags = "theorem%important,corollary%important,proposition%important,%unimportant",
    14.9      document_variants = "document:manual=-proof,-ML,-unimportant"]
   14.10    sessions
   14.11      "HOL-Library"