--- a/src/HOL/Analysis/Interval_Integral.thy Wed Jun 06 13:04:52 2018 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Wed Jun 06 18:19:55 2018 +0200
@@ -88,7 +88,7 @@
from ereal_incseq_approx[OF this] guess X .
then show thesis
apply (intro that[of "\<lambda>i. - X i"])
- apply (auto simp: decseq_def incseq_def reorient: uminus_ereal.simps)
+ apply (auto simp: decseq_def incseq_def simp flip: uminus_ereal.simps)
apply (metis ereal_minus_less_minus ereal_uminus_uminus ereal_Lim_uminus)+
done
qed
@@ -121,7 +121,7 @@
fix x i assume "l i \<le> x" "x \<le> u i"
with \<open>a < ereal (l i)\<close> \<open>ereal (u i) < b\<close>
show "a < ereal x" "ereal x < b"
- by (auto reorient: ereal_less_eq(3))
+ by (auto simp flip: ereal_less_eq(3))
qed
show thesis
by (intro that) fact+
@@ -283,7 +283,7 @@
unfolding interval_lebesgue_integrable_def set_lebesgue_integral_def
apply (rule Bochner_Integration.integral_cong [OF refl])
by (auto simp: einterval_iff ereal_uminus_le_reorder ereal_uminus_less_reorder not_less
- reorient: uminus_ereal.simps
+ simp flip: uminus_ereal.simps
split: split_indicator)
then show ?case
unfolding interval_lebesgue_integral_def
@@ -649,7 +649,7 @@
fix i show "set_integrable lborel {l i .. u i} f"
using \<open>a < l i\<close> \<open>u i < b\<close> unfolding set_integrable_def
by (intro borel_integrable_compact f continuous_at_imp_continuous_on compact_Icc ballI)
- (auto reorient: ereal_less_eq)
+ (auto simp flip: ereal_less_eq)
qed
have 2: "set_borel_measurable lborel (einterval a b) f"
unfolding set_borel_measurable_def