--- a/src/HOL/Probability/Bochner_Integration.thy Sat Nov 14 18:37:49 2015 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy Sun Nov 15 12:39:51 2015 +0100
@@ -886,9 +886,15 @@
intro!: setsum.mono_neutral_cong_left arg_cong2[where f=measure])
qed
+context
+ notes [[inductive_defs]]
+begin
+
inductive integrable for M f where
"has_bochner_integral M f x \<Longrightarrow> integrable M f"
+end
+
definition lebesgue_integral ("integral\<^sup>L") where
"integral\<^sup>L M f = (if \<exists>x. has_bochner_integral M f x then THE x. has_bochner_integral M f x else 0)"