Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Probability/Convolution.thy
changeset 80914 d97fdabd9e2b
parent 62975 1d066f6ab25d 
--- a/src/HOL/Probability/Convolution.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Probability/Convolution.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -11,7 +11,7 @@
 lemma (in finite_measure) sigma_finite_measure: "sigma_finite_measure M"
   ..
 
-definition convolution :: "('a :: ordered_euclidean_space) measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure" (infix "\<star>" 50) where
+definition convolution :: "('a :: ordered_euclidean_space) measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure" (infix \<open>\<star>\<close> 50) where
   "convolution M N = distr (M \<Otimes>\<^sub>M N) borel (\<lambda>(x, y). x + y)"
 
 lemma
isabelle