tuned text
authornipkow
Mon Oct 19 15:58:13 2015 +0200 (2015-10-19)
changeset 614803885464e4874
parent 61479 eec2c9aee907
child 61485 0cc8016cc195
tuned text
src/HOL/Data_Structures/document/root.tex
     1.1 --- a/src/HOL/Data_Structures/document/root.tex	Sun Oct 18 23:03:43 2015 +0200
     1.2 +++ b/src/HOL/Data_Structures/document/root.tex	Mon Oct 19 15:58:13 2015 +0200
     1.3 @@ -37,10 +37,13 @@
     1.4  
     1.5  \section{Bibliographic Notes}
     1.6  
     1.7 -\paragraph{Red-Black trees}
     1.8 +\paragraph{Red-black trees}
     1.9  The insert function follows Okasaki \cite{Okasaki}, the delete function
    1.10  Kahrs \cite{Kahrs-html,Kahrs-JFP01}.
    1.11  
    1.12 +\paragraph{2-3 trees}
    1.13 +The function definitions are based on the teaching material by Franklyn Turbak.
    1.14 +
    1.15  \bibliographystyle{abbrv}
    1.16  \bibliography{root}
    1.17