qualified name to fix integrable_cong ambiguity
authorpaulson <lp15@cam.ac.uk>
Wed, 25 May 2022 10:57:07 +0100
changeset 75957 8e2285baadba
parent 75956 7448423e5dba
child 75958 27745f72e3e1
child 75959 84e6f9b542e2
qualified name to fix integrable_cong ambiguity
src/HOL/Probability/Levy.thy
--- a/src/HOL/Probability/Levy.thy	Tue May 24 16:21:49 2022 +0100
+++ b/src/HOL/Probability/Levy.thy	Wed May 25 10:57:07 2022 +0100
@@ -350,7 +350,7 @@
       hence "complex_integrable (M n) (\<lambda>x. if x = 0 then 0 else 2 * (u  - sin (u * x) / x))"
         using \<open>u > 0\<close>
         unfolding set_integrable_def
-        by (subst integrable_cong) (auto simp add: * simp del: of_real_mult)
+        by (subst Bochner_Integration.integrable_cong) (auto simp add: * simp del: of_real_mult)
       hence **: "integrable (M n) (\<lambda>x. if x = 0 then 0 else 2 * (u  - sin (u * x) / x))"
         unfolding complex_of_real_integrable_eq .
       have "2 * sin x \<le> x" if "2 \<le> x" for x :: real