src/HOL/Probability/Product_PMF.thy
changeset 80914 d97fdabd9e2b
parent 77434 da41823d09a7
--- a/src/HOL/Probability/Product_PMF.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Probability/Product_PMF.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -8,7 +8,7 @@
 begin
 
 text \<open>Conflicting notation from \<^theory>\<open>HOL-Analysis.Infinite_Sum\<close>\<close>
-no_notation Infinite_Sum.abs_summable_on (infixr "abs'_summable'_on" 46)
+no_notation Infinite_Sum.abs_summable_on (infixr \<open>abs'_summable'_on\<close> 46)
 
 subsection \<open>Preliminaries\<close>