--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Wed Feb 01 20:07:13 2023 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Wed Feb 01 20:21:33 2023 +0100
@@ -759,7 +759,7 @@
theorem \<open>Card_order_Times_same_infinite\<close>, which states that self-product
does not increase cardinality -- the proof of this fact adapts a standard
set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11
-at page 47 in @{cite "card-book"}. Then everything else follows fairly easily.\<close>
+at page 47 in \<^cite>\<open>"card-book"\<close>. Then everything else follows fairly easily.\<close>
lemma infinite_iff_card_of_nat:
"\<not> finite A \<longleftrightarrow> ( |UNIV::nat set| \<le>o |A| )"
--- a/src/HOL/Binomial.thy Wed Feb 01 20:07:13 2023 +0100
+++ b/src/HOL/Binomial.thy Wed Feb 01 20:21:33 2023 +0100
@@ -718,7 +718,7 @@
using binomial_symmetric[of k n] by (simp add: binomial_gbinomial [symmetric])
-text \<open>The absorption identity (equation 5.5 @{cite \<open>p.~157\<close> GKP_CM}):
+text \<open>The absorption identity (equation 5.5 \<^cite>\<open>\<open>p.~157\<close> in GKP_CM\<close>):
\[
{r \choose k} = \frac{r}{k}{r - 1 \choose k - 1},\quad \textnormal{integer } k \neq 0.
\]\<close>
@@ -728,7 +728,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 \<open>p.~157\<close> GKP_CM}:
+restriction \<^cite>\<open>\<open>p.~157\<close> in GKP_CM\<close>:
\[
k{r \choose k} = r{r - 1 \choose k - 1}, \quad \textnormal{integer } k.
\]\<close>
@@ -740,7 +740,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 \<open>p.~157\<close> GKP_CM}:\<close>
+ following the proof by GKP \<^cite>\<open>\<open>p.~157\<close> in GKP_CM\<close>:\<close>
lemma binomial_absorb_comp: "(n - k) * (n choose k) = n * ((n - 1) choose k)"
(is "?lhs = ?rhs")
proof (cases "n \<le> k")
@@ -771,7 +771,7 @@
by (subst choose_reduce_nat) simp_all
text \<open>
- Equation 5.9 of the reference material @{cite \<open>p.~159\<close> GKP_CM} is a useful
+ Equation 5.9 of the reference material \<^cite>\<open>\<open>p.~159\<close> in GKP_CM\<close> is a useful
summation formula, operating on both indices:
\[
\sum\limits_{k \leq n}{r + k \choose k} = {r + n + 1 \choose n},
@@ -793,7 +793,7 @@
subsubsection \<open>Summation on the upper index\<close>
text \<open>
- Another summation formula is equation 5.10 of the reference material @{cite \<open>p.~160\<close> GKP_CM},
+ Another summation formula is equation 5.10 of the reference material \<^cite>\<open>\<open>p.~160\<close> in GKP_CM\<close>,
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>
--- a/src/HOL/GCD.thy Wed Feb 01 20:07:13 2023 +0100
+++ b/src/HOL/GCD.thy Wed Feb 01 20:21:33 2023 +0100
@@ -2011,7 +2011,7 @@
lemma gcd_mult_distrib_nat: "k * gcd m n = gcd (k * m) (k * n)"
for k m n :: nat
- \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
+ \<comment> \<open>\<^cite>\<open>\<open>page 27\<close> in davenport92\<close>\<close>
by (simp add: gcd_mult_left)
lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)"
--- a/src/HOL/HOL.thy Wed Feb 01 20:07:13 2023 +0100
+++ b/src/HOL/HOL.thy Wed Feb 01 20:21:33 2023 +0100
@@ -57,7 +57,7 @@
subsection \<open>Primitive logic\<close>
text \<open>
-The definition of the logic is based on Mike Gordon's technical report @{cite "Gordon-TR68"} that
+The definition of the logic is based on Mike Gordon's technical report \<^cite>\<open>"Gordon-TR68"\<close> that
describes the first implementation of HOL. However, there are a number of differences.
In particular, we start with the definite description operator and introduce Hilbert's \<open>\<epsilon>\<close> operator
only much later. Moreover, axiom \<open>(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)\<close> is derived from the other
--- a/src/HOL/Wellfounded.thy Wed Feb 01 20:07:13 2023 +0100
+++ b/src/HOL/Wellfounded.thy Wed Feb 01 20:21:33 2023 +0100
@@ -617,7 +617,7 @@
text \<open>
Inductive definition of the accessible part \<open>acc r\<close> of a
- relation; see also @{cite "paulin-tlca"}.
+ relation; see also \<^cite>\<open>"paulin-tlca"\<close>.
\<close>
inductive_set acc :: "('a \<times> 'a) set \<Rightarrow> 'a set" for r :: "('a \<times> 'a) set"