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/Analysis/Binary_Product_Measure.thy
changeset 80914 d97fdabd9e2b
parent 77179 6d2ca97a8f46 
--- a/src/HOL/Analysis/Binary_Product_Measure.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -16,7 +16,7 @@
 
 subsection "Binary products"
 
-definition\<^marker>\<open>tag important\<close> pair_measure (infixr "\<Otimes>\<^sub>M" 80) where
+definition\<^marker>\<open>tag important\<close> pair_measure (infixr \<open>\<Otimes>\<^sub>M\<close> 80) where
   "A \<Otimes>\<^sub>M B = measure_of (space A \<times> space B)
       {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B}
       (\<lambda>X. \<integral>\<^sup>+x. (\<integral>\<^sup>+y. indicator X (x,y) \<partial>B) \<partial>A)"
isabelle