# HG changeset patch
# User wenzelm
# Date 1711021671 -3600
# Node ID 82aaa0d8fc3bf34bdd1353f09231e7f49ecd66e7
# Parent  67d28b35c5d8e25cf6d7ab2929b9d0fdc6dc1941
isabelle update -u cite;

diff -r 67d28b35c5d8 -r 82aaa0d8fc3b src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Wed Mar 20 21:12:49 2024 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy	Thu Mar 21 12:47:51 2024 +0100
@@ -1745,11 +1745,11 @@
 subsection \<open>Averaging Theorem\<close>
 
 text \<open>We aim to lift results from the real case to arbitrary Banach spaces. 
-      Our fundamental tool in this regard will be the averaging theorem. The proof of this theorem is due to Serge Lang (Real and Functional Analysis) \cite{Lang_1993}. 
+      Our fundamental tool in this regard will be the averaging theorem. The proof of this theorem is due to Serge Lang (Real and Functional Analysis) \<^cite>\<open>"Lang_1993"\<close>. 
       The theorem allows us to make statements about a function's value almost everywhere, depending on the value its integral takes on various sets of the measure space.\<close>
 
 text \<open>Before we introduce and prove the averaging theorem, we will first show the following lemma which is crucial for our proof. 
-      While not stated exactly in this manner, our proof makes use of the characterization of second-countable topological spaces given in the book General Topology by Ryszard Engelking (Theorem 4.1.15) \cite{engelking_1989}.
+      While not stated exactly in this manner, our proof makes use of the characterization of second-countable topological spaces given in the book General Topology by Ryszard Engelking (Theorem 4.1.15) \<^cite>\<open>"engelking_1989"\<close>.
     (Engelking's book \emph{General Topology})\<close>
 
 lemma balls_countable_basis:
diff -r 67d28b35c5d8 -r 82aaa0d8fc3b src/HOL/Library/Centered_Division.thy
--- a/src/HOL/Library/Centered_Division.thy	Wed Mar 20 21:12:49 2024 +0100
+++ b/src/HOL/Library/Centered_Division.thy	Thu Mar 21 12:47:51 2024 +0100
@@ -15,7 +15,7 @@
   \noindent The following specification of division on integers centers
   the modulus around zero.  This is useful e.g.~to define division
   on Gauss numbers.
-  N.b.: This is not mentioned \cite{leijen01}.
+  N.b.: This is not mentioned \<^cite>\<open>"leijen01"\<close>.
 \<close>
 
 definition centered_divide :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>  (infixl \<open>cdiv\<close> 70)
diff -r 67d28b35c5d8 -r 82aaa0d8fc3b src/HOL/Library/Signed_Division.thy
--- a/src/HOL/Library/Signed_Division.thy	Wed Mar 20 21:12:49 2024 +0100
+++ b/src/HOL/Library/Signed_Division.thy	Thu Mar 21 12:47:51 2024 +0100
@@ -48,7 +48,7 @@
 end
 
 text \<open>
-  \noindent The following specification of division is named ``T-division'' in \cite{leijen01}.
+  \noindent The following specification of division is named ``T-division'' in \<^cite>\<open>"leijen01"\<close>.
   It is motivated by ISO C99, which in turn adopted the typical behavior of
   hardware modern in the beginning of the 1990ies; but note ISO C99 describes
   the instance on machine words, not mathematical integers.
diff -r 67d28b35c5d8 -r 82aaa0d8fc3b src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Wed Mar 20 21:12:49 2024 +0100
+++ b/src/HOL/Library/Word.thy	Thu Mar 21 12:47:51 2024 +0100
@@ -626,7 +626,7 @@
 
 text \<open>
   The following specification of word division just lifts the pre-existing
-  division on integers named ``F-Division'' in \cite{leijen01}.
+  division on integers named ``F-Division'' in \<^cite>\<open>"leijen01"\<close>.
 \<close>
 
 instantiation word :: (len) semiring_modulo