src/ZF/QPair.thy
changeset 81125 ec121999a9cb
parent 80917 2a77bc3b4eac
--- a/src/ZF/QPair.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/QPair.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -21,8 +21,8 @@
 \<close>
 
 definition
-  QPair     :: "[i, i] \<Rightarrow> i"                      (\<open><(_;/ _)>\<close>)  where
-    "<a;b> \<equiv> a+b"
+  QPair     :: "[i, i] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix Quine pair\<close>\<close><_;/ _>)\<close>)
+  where "<a;b> \<equiv> a+b"
 
 definition
   qfst :: "i \<Rightarrow> i"  where