--- a/src/HOL/Analysis/Set_Integral.thy Thu Apr 12 12:16:34 2018 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy Fri Apr 13 15:58:27 2018 +0100
@@ -67,6 +67,9 @@
by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
qed
+lemma set_lebesgue_integral_zero [simp]: "set_lebesgue_integral M A (\<lambda>x. 0) = 0"
+ by (auto simp: set_lebesgue_integral_def)
+
lemma set_lebesgue_integral_cong:
assumes "A \<in> sets M" and "\<forall>x. x \<in> A \<longrightarrow> f x = g x"
shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"