# HG changeset patch
# User wenzelm
# Date 1424699320 -3600
# Node ID c422ef7b9fae33f4a2bc1cb1a806c7412ad01edf
# Parent  19356bb4a0dbc8feef02dda4279ff4844542d5e2
proper LaTeX;

diff -r 19356bb4a0db -r c422ef7b9fae src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Mon Feb 23 14:48:17 2015 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy	Mon Feb 23 14:48:40 2015 +0100
@@ -614,7 +614,7 @@
 text{*Versions of the theorems above for the natural-number version of "choose"*}
 lemma binomial_altdef_of_nat:
   fixes n k :: nat
-    and x :: "'a :: {field_char_0,field_inverse_zero}"  --{*the point is to constrain @{typ 'a}}*}
+    and x :: "'a :: {field_char_0,field_inverse_zero}"  --{*the point is to constrain @{typ 'a}*}
   assumes "k \<le> n"
   shows "of_nat (n choose k) = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
 using assms