src/HOL/Data_Structures/document/root.tex

--- a/src/HOL/Data_Structures/document/root.tex	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Data_Structures/document/root.tex	Fri Oct 30 20:01:05 2015 +0100
@@ -44,6 +44,10 @@
 \paragraph{2-3 trees}
 The function definitions are based on the teaching material by Franklyn Turbak.
 
+\paragraph{Splay trees}
+They were invented by Sleator and Tarjan \cite{SleatorT-JACM85}.
+Our formalisation follows Schoenmakers \cite{Schoenmakers-IPL93}.
+
 \bibliographystyle{abbrv}
 \bibliography{root}