# HG changeset patch
# User wenzelm
# Date 1675279293 -3600
# Node ID 816959264c326d3c9c000683196cadb61776cb62
# Parent  e0e9f1b4c844c358c5e922defd09220d1ca3b1e3
isabelle update -u cite -l "";

diff -r e0e9f1b4c844 -r 816959264c32 src/HOL/BNF_Cardinal_Order_Relation.thy
--- 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| )"
diff -r e0e9f1b4c844 -r 816959264c32 src/HOL/Binomial.thy
--- 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>
diff -r e0e9f1b4c844 -r 816959264c32 src/HOL/GCD.thy
--- 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)"
diff -r e0e9f1b4c844 -r 816959264c32 src/HOL/HOL.thy
--- 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
diff -r e0e9f1b4c844 -r 816959264c32 src/HOL/Wellfounded.thy
--- 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"