src/HOL/HOLCF/Sprod.thy

--- a/src/HOL/HOLCF/Sprod.thy	Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/HOLCF/Sprod.thy	Sun Aug 25 21:10:01 2024 +0200
@@ -41,6 +41,7 @@
   where "ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
 
 syntax "_stuple" :: "[logic, args] \<Rightarrow> logic"  ("(1'(:_,/ _:'))")
+syntax_consts "_stuple" \<rightleftharpoons> spair
 translations
   "(:x, y, z:)" \<rightleftharpoons> "(:x, (:y, z:):)"
   "(:x, y:)" \<rightleftharpoons> "CONST spair\<cdot>x\<cdot>y"