diff -r aaa31cd0caef -r f13796496e82 src/HOL/Data_Structures/document/root.tex --- a/src/HOL/Data_Structures/document/root.tex Sun Apr 08 11:05:52 2018 +0200 +++ b/src/HOL/Data_Structures/document/root.tex Sun Apr 08 12:14:00 2018 +0200 @@ -65,6 +65,10 @@ They were invented by Sleator and Tarjan \cite{SleatorT-JACM85}. Our formalisation follows Schoenmakers \cite{Schoenmakers-IPL93}. +\paragraph{Join-based BSTs} +They were invented by Adams \cite{Adams-TR92,Adams-JFP93} +and analyzed by Blelloch \emph{et al.} \cite{BlellochFS-SPAA16}. + \paragraph{Leftist heaps} They were invented by Crane \cite{Crane72}. A first functional implementation is due to N\'u\~{n}ez \emph{et al.}~\cite{NunezPP95}.