src/ZF/QPair.thy
changeset 80917 2a77bc3b4eac
parent 80761 bc936d3d8b45
child 81125 ec121999a9cb
--- a/src/ZF/QPair.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/QPair.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -45,7 +45,7 @@
     "QSigma(A,B)  \<equiv>  \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}"
 
 syntax
-  "_QSUM"   :: "[idt, i, i] \<Rightarrow> i"               (\<open>(3QSUM _ \<in> _./ _)\<close> 10)
+  "_QSUM"   :: "[idt, i, i] \<Rightarrow> i"  (\<open>(\<open>indent=3 notation=\<open>binder QSUM\<in>\<close>\<close>QSUM _ \<in> _./ _)\<close> 10)
 syntax_consts
   "_QSUM" \<rightleftharpoons> QSigma
 translations