--- a/src/HOL/Data_Structures/document/root.tex Wed Mar 23 16:37:19 2016 +0100
+++ b/src/HOL/Data_Structures/document/root.tex Thu Mar 24 15:56:47 2016 +0100
@@ -63,6 +63,10 @@
They were invented by Sleator and Tarjan \cite{SleatorT-JACM85}.
Our formalisation follows Schoenmakers \cite{Schoenmakers-IPL93}.
+\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}.
+
\bibliographystyle{abbrv}
\bibliography{root}