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