# HG changeset patch
# User nipkow
# Date 1449332630 -3600
# Node ID 21502fb1ff0a8c1b8f1b476ba8b0de1dab48af82
# Parent  0494964bb2261104661a7d231f013fdf995cb439
tuned

diff -r 0494964bb226 -r 21502fb1ff0a src/HOL/Data_Structures/document/root.bib
--- 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}
 
diff -r 0494964bb226 -r 21502fb1ff0a src/HOL/Data_Structures/document/root.tex
--- 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}.