--- a/src/HOL/Data_Structures/document/root.tex Thu Aug 06 17:11:33 2020 +0200
+++ b/src/HOL/Data_Structures/document/root.tex Thu Aug 06 17:39:57 2020 +0200
@@ -51,7 +51,7 @@
O'Donnell~\cite{HoffmannOD-TOPLAS82} (only insertion)
and Reade \cite{Reade-SCP92}.
Our formalisation is based on the teaching material by
-Turbak~\cite{Turbak230} .
+Turbak~\cite{Turbak230} and the article by Hinze~\cite{jfp/Hinze18}.
\paragraph{1-2 brother trees}
They were invented by Ottmann and Six~\cite{OttmannS76,OttmannW-CJ80}.