src/HOL/Data_Structures/document/root.tex
changeset 61224 759b5299a9f2
parent 61203 a8a8eca85801
child 61480 3885464e4874
--- a/src/HOL/Data_Structures/document/root.tex	Mon Sep 21 23:22:11 2015 +0200
+++ b/src/HOL/Data_Structures/document/root.tex	Tue Sep 22 08:38:25 2015 +0200
@@ -29,14 +29,19 @@
 of a textbook than a library of efficient algorithms.
 \end{abstract}
 
-\setcounter{tocdepth}{2}
+\setcounter{tocdepth}{1}
 \tableofcontents
 \newpage
 
-% generated text of all theories
 \input{session}
 
-%\bibliographystyle{abbrv}
-%\bibliography{root}
+\section{Bibliographic Notes}
+
+\paragraph{Red-Black trees}
+The insert function follows Okasaki \cite{Okasaki}, the delete function
+Kahrs \cite{Kahrs-html,Kahrs-JFP01}.
+
+\bibliographystyle{abbrv}
+\bibliography{root}
 
 \end{document}