--- a/src/HOL/HOLCF/Sprod.thy Tue Oct 01 22:12:11 2024 +0200
+++ b/src/HOL/HOLCF/Sprod.thy Tue Oct 01 23:36:10 2024 +0200
@@ -16,7 +16,7 @@
definition "sprod = {p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
-pcpodef ('a, 'b) sprod (\<open>(_ \<otimes>/ _)\<close> [21,20] 20) = "sprod :: ('a \<times> 'b) set"
+pcpodef ('a, 'b) sprod (\<open>(\<open>notation=\<open>infix strict product\<close>\<close>_ \<otimes>/ _)\<close> [21,20] 20) = "sprod :: ('a \<times> 'b) set"
by (simp_all add: sprod_def)
instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin