# HG changeset patch
# User hoelzl
# Date 1465481493 -7200
# Node ID e497387de7af484fcf5d7b7463c91c44b141cf3d
# Parent  90a44d2716837bef7fb1579ca17ea8d8c138cc34
remove smt call in Lebesge_Measure

diff -r 90a44d271683 -r e497387de7af src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Jun 08 19:36:45 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Thu Jun 09 16:11:33 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)+
diff -r 90a44d271683 -r e497387de7af src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Jun 08 19:36:45 2016 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Thu Jun 09 16:11:33 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"