src/HOL/Probability/Interval_Integral.thy
changeset 59867 58043346ca64
parent 59587 8ea7b22525cb
child 61609 77b453bd616f
     1.1 --- a/src/HOL/Probability/Interval_Integral.thy	Tue Mar 31 16:49:41 2015 +0100
     1.2 +++ b/src/HOL/Probability/Interval_Integral.thy	Tue Mar 31 21:54:32 2015 +0200
     1.3 @@ -220,7 +220,7 @@
     1.4    by (simp add: interval_lebesgue_integrable_def)
     1.5  
     1.6  lemma interval_lebesgue_integrable_divide [intro, simp]:
     1.7 -  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field_inverse_zero, second_countable_topology}"
     1.8 +  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}"
     1.9    shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
    1.10      interval_lebesgue_integrable M a b (\<lambda>x. f x / c)"
    1.11    by (simp add: interval_lebesgue_integrable_def)
    1.12 @@ -238,7 +238,7 @@
    1.13    by (simp add: interval_lebesgue_integral_def)
    1.14  
    1.15  lemma interval_lebesgue_integral_divide [simp]:
    1.16 -  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field_inverse_zero, second_countable_topology}"
    1.17 +  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}"
    1.18    shows "interval_lebesgue_integral M a b (\<lambda>x. f x / c) =
    1.19      interval_lebesgue_integral M a b f / c"
    1.20    by (simp add: interval_lebesgue_integral_def)