--- a/src/HOL/Binomial.thy Fri Dec 29 18:09:38 2017 +0100
+++ b/src/HOL/Binomial.thy Fri Dec 29 19:17:52 2017 +0100
@@ -708,7 +708,7 @@
using binomial_symmetric[of k n] by (simp add: binomial_gbinomial [symmetric])
-text \<open>The absorption identity (equation 5.5 \cite[p.~157]{GKP}):
+text \<open>The absorption identity (equation 5.5 @{cite \<open>p.~157\<close> GKP_CM}):
\[
{r \choose k} = \frac{r}{k}{r - 1 \choose k - 1},\quad \textnormal{integer } k \neq 0.
\]\<close>
@@ -718,7 +718,7 @@
text \<open>The absorption identity is written in the following form to avoid
division by $k$ (the lower index) and therefore remove the $k \neq 0$
-restriction\cite[p.~157]{GKP}:
+restriction @{cite \<open>p.~157\<close> GKP_CM}:
\[
k{r \choose k} = r{r - 1 \choose k - 1}, \quad \textnormal{integer } k.
\]\<close>
@@ -730,7 +730,7 @@
by (cases n) (simp_all add: binomial_eq_0 Suc_times_binomial del: binomial_Suc_Suc mult_Suc)
text \<open>The absorption companion identity for natural number coefficients,
- following the proof by GKP \cite[p.~157]{GKP}:\<close>
+ following the proof by GKP @{cite \<open>p.~157\<close> GKP_CM}:\<close>
lemma binomial_absorb_comp: "(n - k) * (n choose k) = n * ((n - 1) choose k)"
(is "?lhs = ?rhs")
proof (cases "n \<le> k")
@@ -761,7 +761,7 @@
by (subst choose_reduce_nat) simp_all
text \<open>
- Equation 5.9 of the reference material \cite[p.~159]{GKP} is a useful
+ Equation 5.9 of the reference material @{cite \<open>p.~159\<close> GKP_CM} is a useful
summation formula, operating on both indices:
\[
\sum\limits_{k \leq n}{r + k \choose k} = {r + n + 1 \choose n},
@@ -783,7 +783,7 @@
subsubsection \<open>Summation on the upper index\<close>
text \<open>
- Another summation formula is equation 5.10 of the reference material \cite[p.~160]{GKP},
+ Another summation formula is equation 5.10 of the reference material @{cite \<open>p.~160\<close> GKP_CM},
aptly named \emph{summation on the upper index}:\[\sum_{0 \leq k \leq n} {k \choose m} =
{n + 1 \choose m + 1}, \quad \textnormal{integers } m, n \geq 0.\]
\<close>