src/HOL/Analysis/Interval_Integral.thy
changeset 63886 685fb01256af
parent 63627 6ddb43c6b711
child 63941 f353674c2528
     1.1 --- a/src/HOL/Analysis/Interval_Integral.thy	Thu Sep 15 22:41:05 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Interval_Integral.thy	Fri Sep 16 13:56:51 2016 +0200
     1.3 @@ -311,7 +311,7 @@
     1.4                     ereal_uminus_le_reorder ereal_uminus_less_reorder not_less
     1.5                     uminus_ereal.simps[symmetric]
     1.6               simp del: uminus_ereal.simps
     1.7 -             intro!: integral_cong
     1.8 +             intro!: Bochner_Integration.integral_cong
     1.9               split: split_indicator)
    1.10  qed
    1.11