--- a/src/HOL/Data_Structures/document/root.tex Tue Jan 07 07:03:18 2020 +0100
+++ b/src/HOL/Data_Structures/document/root.tex Tue Jan 07 12:37:12 2020 +0100
@@ -42,8 +42,9 @@
\section{Bibliographic Notes}
\paragraph{Red-black trees}
-The insert function follows Okasaki \cite{Okasaki}, the delete function
-Kahrs \cite{Kahrs-html,Kahrs-JFP01}.
+The insert function follows Okasaki \cite{Okasaki}. The delete function
+in theory \isa{RBT\_Set} follows Kahrs \cite{Kahrs-html,Kahrs-JFP01},
+an alternative delete function is given in theory \isa{RBT\_Set2}.
\paragraph{2-3 trees}
Equational definitions were given by Hoffmann and