--- a/src/HOL/Analysis/Interval_Integral.thy Wed Mar 31 11:24:46 2021 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Wed Mar 31 18:18:03 2021 +0200
@@ -438,8 +438,9 @@
by (rule interval_integral_endpoints_reverse)
show ?thesis
using integrable
- by (cases a b b c a c rule: linorder_le_cases[case_product linorder_le_cases linorder_cases])
- (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3)
+ apply (cases a b b c a c rule: linorder_le_cases[case_product linorder_le_cases linorder_cases])
+ apply simp_all (* remove some looping cases *)
+ by (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3)
qed
lemma interval_integrable_isCont: