--- a/src/HOL/Library/Ramsey.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Library/Ramsey.thy Fri Sep 20 19:51:08 2024 +0200
@@ -15,7 +15,7 @@
subsubsection \<open>The $n$-element subsets of a set $A$\<close>
-definition nsets :: "['a set, nat] \<Rightarrow> 'a set set" ("([_]\<^bsup>_\<^esup>)" [0,999] 999)
+definition nsets :: "['a set, nat] \<Rightarrow> 'a set set" (\<open>([_]\<^bsup>_\<^esup>)\<close> [0,999] 999)
where "nsets A n \<equiv> {N. N \<subseteq> A \<and> finite N \<and> card N = n}"
lemma finite_imp_finite_nsets: "finite A \<Longrightarrow> finite ([A]\<^bsup>k\<^esup>)"