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>