--- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Tue Apr 06 18:12:20 2021 +0000
+++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Wed Apr 07 12:28:19 2021 +0000
@@ -881,7 +881,7 @@
finally have le: "emeasure lebesgue (-T \<inter> U) < ennreal (1 / 2^n)"
by (simp add: eq)
have 1: "continuous_on (T \<union> -U) (indicat_real S)"
- unfolding indicator_def
+ unfolding indicator_def of_bool_def
proof (rule continuous_on_cases [OF \<open>closed T\<close>])
show "closed (- U)"
using \<open>open U\<close> by blast
@@ -976,7 +976,7 @@
using nn
by (auto simp: inj_on_def intro: sum.cong)
finally show ?thesis
- by (subst *) (simp add: enn2real_sum indicator_def if_distrib cong: if_cong)
+ by (subst *) (simp add: enn2real_sum indicator_def of_bool_def if_distrib cong: if_cong)
qed
lemma\<^marker>\<open>tag important\<close> simple_function_induct_real