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