src/ZF/QPair.thy

--- a/src/ZF/QPair.thy	Fri Aug 23 22:47:51 2024 +0200
+++ b/src/ZF/QPair.thy	Fri Aug 23 23:14:39 2024 +0200
@@ -48,6 +48,8 @@
   "_QSUM"   :: "[idt, i, i] \<Rightarrow> i"               (\<open>(3QSUM _ \<in> _./ _)\<close> 10)
 translations
   "QSUM x \<in> A. B" => "CONST QSigma(A, \<lambda>x. B)"
+syntax_consts
+  "_QSUM" \<rightleftharpoons> QSigma
 
 abbreviation
   qprod  (infixr \<open><*>\<close> 80) where