src/HOL/Binomial.thy

--- a/src/HOL/Binomial.thy	Wed Dec 11 11:14:50 2024 +0100
+++ b/src/HOL/Binomial.thy	Wed Dec 11 11:18:52 2024 +0100
@@ -18,8 +18,13 @@
 
 text \<open>Combinatorial definition\<close>
 
-definition binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat"  (infix \<open>choose\<close> 64)
-  where "n choose k = card {K\<in>Pow {0..<n}. card K = k}"
+definition binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  where "binomial n k = card {K\<in>Pow {0..<n}. card K = k}"
+
+open_bundle binomial_syntax
+begin
+notation binomial  (infix \<open>choose\<close> 64)
+end
 
 lemma binomial_right_mono:
   assumes "m \<le> n" shows "m choose k \<le> n choose k"