--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Thu Jun 09 16:04:20 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Thu Jun 09 16:42:10 2016 +0200
@@ -6289,13 +6289,13 @@
obtain B where B: "\<And>x. B \<le> cmod x \<Longrightarrow> norm (f x) * 2 < cmod (f z)"
by (auto simp: dist_norm)
define R where "R = 1 + \<bar>B\<bar> + norm z"
- have "R > 0" unfolding R_def
+ have "R > 0" unfolding R_def
proof -
have "0 \<le> cmod z + \<bar>B\<bar>"
by (metis (full_types) add_nonneg_nonneg norm_ge_zero real_norm_def)
then show "0 < 1 + \<bar>B\<bar> + cmod z"
by linarith
- qed
+ qed
have *: "((\<lambda>u. f u / (u - z)) has_contour_integral 2 * complex_of_real pi * \<i> * f z) (circlepath z R)"
apply (rule Cauchy_integral_circlepath)
using \<open>R > 0\<close> apply (auto intro: holomorphic_on_subset [OF holf] holomorphic_on_imp_continuous_on)+
--- a/src/HOL/Probability/Lebesgue_Measure.thy Thu Jun 09 16:04:20 2016 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Thu Jun 09 16:42:10 2016 +0200
@@ -526,11 +526,12 @@
shows "emeasure lborel A = 0"
proof -
have "A \<subseteq> (\<Union>i. {from_nat_into A i})" using from_nat_into_surj assms by force
- moreover have "emeasure lborel (\<Union>i. {from_nat_into A i}) = 0"
+ then have "emeasure lborel A \<le> emeasure lborel (\<Union>i. {from_nat_into A i})"
+ by (intro emeasure_mono) auto
+ also have "emeasure lborel (\<Union>i. {from_nat_into A i}) = 0"
by (rule emeasure_UN_eq_0) auto
- ultimately have "emeasure lborel A \<le> 0" using emeasure_mono
- by (smt UN_E emeasure_empty equalityI from_nat_into order_refl singletonD subsetI)
- thus ?thesis by (auto simp add: )
+ finally show ?thesis
+ by (auto simp add: )
qed
lemma countable_imp_null_set_lborel: "countable A \<Longrightarrow> A \<in> null_sets lborel"