# HG changeset patch
# User paulson
# Date 979318812 -3600
# Node ID f321d21b9a6b4818384f838f472bb061809b0ab8
# Parent  7fb42b97413a6fa7b4bf1d50817b247d6638ddc0
LateX-2e moans about using \\choose

diff -r 7fb42b97413a -r f321d21b9a6b doc-src/TutorialI/Sets/sets.tex
--- a/doc-src/TutorialI/Sets/sets.tex	Fri Jan 12 17:59:37 2001 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Fri Jan 12 18:00:12 2001 +0100
@@ -402,7 +402,7 @@
 \rulename{n_subsets}
 \end{isabelle}
 Writing $|A|$ as $n$, the last of these theorems says that the number of
-$k$-element subsets of~$A$ is $n \choose k$.
+$k$-element subsets of~$A$ is $\binom{n}{k}$.
 
 \begin{warn}
 The term \isa{Finite\ A} is an abbreviation for