--- a/src/HOL/Library/Poly_Mapping.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Library/Poly_Mapping.thy Sun Jan 15 18:30:18 2023 +0100
@@ -295,7 +295,7 @@
to coefficients. Lets call this the \emph{ultimate interpretation}.
\item A further more specialised type isomorphic to @{typ "nat \<Rightarrow>\<^sub>0 'a"}
is apt to direct implementation using code generation
- \cite{Haftmann-Nipkow:2010:code}.
+ \<^cite>\<open>"Haftmann-Nipkow:2010:code"\<close>.
\end{enumerate}
Note that despite the names \emph{mapping} and \emph{lookup} suggest something
implementation-near, it is best to keep @{typ "'a \<Rightarrow>\<^sub>0 'b"} as an abstract