diff -r 6ce0c8d59f5a -r ec121999a9cb src/ZF/QPair.thy --- 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 @@ \ definition - QPair :: "[i, i] \ i" (\<(_;/ _)>\) where - " \ a+b" + QPair :: "[i, i] \ i" (\(\indent=1 notation=\mixfix Quine pair\\<_;/ _>)\) + where " \ a+b" definition qfst :: "i \ i" where