--- 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:
--- 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)
--- 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.
--- 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