# HG changeset patch
# User nipkow
# Date 1445263093 -7200
# Node ID 3885464e4874eba18790d2e4aa26857aba343072
# Parent  eec2c9aee907b56139b07a0ac1e86b74c7af7443
tuned text

diff -r eec2c9aee907 -r 3885464e4874 src/HOL/Data_Structures/document/root.tex
--- a/src/HOL/Data_Structures/document/root.tex	Sun Oct 18 23:03:43 2015 +0200
+++ b/src/HOL/Data_Structures/document/root.tex	Mon Oct 19 15:58:13 2015 +0200
@@ -37,10 +37,13 @@
 
 \section{Bibliographic Notes}
 
-\paragraph{Red-Black trees}
+\paragraph{Red-black trees}
 The insert function follows Okasaki \cite{Okasaki}, the delete function
 Kahrs \cite{Kahrs-html,Kahrs-JFP01}.
 
+\paragraph{2-3 trees}
+The function definitions are based on the teaching material by Franklyn Turbak.
+
 \bibliographystyle{abbrv}
 \bibliography{root}