--- a/src/HOL/Data_Structures/document/root.tex Thu Dec 03 15:33:01 2015 +0100
+++ b/src/HOL/Data_Structures/document/root.tex Fri Dec 04 14:39:31 2015 +0100
@@ -45,6 +45,10 @@
The function definitions are based on the teaching material by
Turbak~\cite{Turbak230}.
+\paragraph{1-2 brother trees}
+They were invented by Ottmann and Six~\cite{OttmannS76,OttmannW-CJ80}.
+The functional version is due to Hinze~\cite{Hinze-bro12}.
+
\paragraph{Splay trees}
They were invented by Sleator and Tarjan \cite{SleatorT-JACM85}.
Our formalisation follows Schoenmakers \cite{Schoenmakers-IPL93}.