--- a/src/HOL/Data_Structures/document/root.bib Sat Dec 05 16:33:20 2015 +0100
+++ b/src/HOL/Data_Structures/document/root.bib Sat Dec 05 17:23:50 2015 +0100
@@ -3,6 +3,11 @@
journal={J. Functional Programming},
volume=19,number={6},pages={633--644},year=2009}
+@article{HoffmannOD-TOPLAS82,
+author={Christoph M. Hoffmann and Michael J. O'Donnell},
+title={Programming with Equations},journal={{ACM} Trans. Program. Lang. Syst.},
+volume=4,number=1,pages={83--112},year=1982}}
+
@article{Kahrs-JFP01,author={Stefan Kahrs},title={Red-Black Trees with Types},
journal={J. Functional Programming},volume=11,number=4,pages={425-432},year=2001}
@@ -20,6 +25,10 @@
title={1-2 Brother Trees or {AVL} Trees Revisited},journal={Comput. J.},
volume=23,number=3,pages={248--255},year=1980}
+@article{Reade-SCP92,author={Chris Reade},
+title={Balanced Trees with Removals: An Exercise in Rewriting and Proof},
+journal={Sci. Comput. Program.},volume=18,number=2,pages={181--204},year=1992}
+
@article{Schoenmakers-IPL93,author="Berry Schoenmakers",
title="A Systematic Analysis of Splaying",journal={Information Processing Letters},volume=45,pages={41-50},year=1993}
--- a/src/HOL/Data_Structures/document/root.tex Sat Dec 05 16:33:20 2015 +0100
+++ b/src/HOL/Data_Structures/document/root.tex Sat Dec 05 17:23:50 2015 +0100
@@ -42,8 +42,11 @@
Kahrs \cite{Kahrs-html,Kahrs-JFP01}.
\paragraph{2-3 trees}
-The function definitions are based on the teaching material by
-Turbak~\cite{Turbak230}.
+Equational definitions were given by Hoffmann and
+O'Donnell~\cite{HoffmannOD-TOPLAS82} (only insertion)
+and Reade \cite{Reade-SCP92}.
+Our formalisation is 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}.