src/HOL/Data_Structures/document/root.tex
changeset 62706 49c6a54ceab6
parent 62496 f187aaf602c4
child 64318 1e92b5c35615
equal deleted inserted replaced
62700:e3ca8dc01c4f 62706:49c6a54ceab6
    61 
    61 
    62 \paragraph{Splay trees}
    62 \paragraph{Splay trees}
    63 They were invented by Sleator and Tarjan \cite{SleatorT-JACM85}.
    63 They were invented by Sleator and Tarjan \cite{SleatorT-JACM85}.
    64 Our formalisation follows Schoenmakers \cite{Schoenmakers-IPL93}.
    64 Our formalisation follows Schoenmakers \cite{Schoenmakers-IPL93}.
    65 
    65 
       
    66 \paragraph{Leftist heaps}
       
    67 They were invented by Crane \cite{Crane72}. A first functional implementation
       
    68 is due to N\'u\~{n}ez \emph{et al.}~\cite{NunezPP95}.
       
    69 
    66 \bibliographystyle{abbrv}
    70 \bibliographystyle{abbrv}
    67 \bibliography{root}
    71 \bibliography{root}
    68 
    72 
    69 \end{document}
    73 \end{document}