--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Mon Sep 23 13:32:38 2024 +0200
@@ -117,7 +117,7 @@
We shall prove that this notion is unique up to order isomorphism, meaning
that order isomorphism shall be the true identity of cardinals.\<close>
-definition card_of :: "'a set \<Rightarrow> 'a rel" ("|_|" )
+definition card_of :: "'a set \<Rightarrow> 'a rel" (\<open>|_|\<close> )
where "card_of A = (SOME r. card_order_on A r)"
lemma card_of_card_order_on: "card_order_on A |A|"