src/HOL/Analysis/Interval_Integral.thy

 proof -
   have "-b < -a" using \<open>a < b\<close> by simp
   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
 
 lemma einterval_Icc_approximation:

       by (auto intro: less_imp_le simp: eventually_sequentially)
   next
     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+
 qed
 

   case (le a b) 
   have "LBINT x:{x. - x \<in> einterval a b}. f (- x) = LBINT x:einterval (- b) (- a). f (- x)"
     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 
     by (subst set_integral_reflect) (simp add: le)
 qed

   have 1: "\<And>i. set_integrable lborel {l i..u i} f"
   proof -
     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
     by (auto simp del: real_scaleR_def intro!: borel_measurable_continuous_on_indicator
              simp: continuous_on_eq_continuous_at einterval_iff f)