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}