equal
deleted
inserted
replaced
40 \paragraph{Red-black trees} |
40 \paragraph{Red-black trees} |
41 The insert function follows Okasaki \cite{Okasaki}, the delete function |
41 The insert function follows Okasaki \cite{Okasaki}, the delete function |
42 Kahrs \cite{Kahrs-html,Kahrs-JFP01}. |
42 Kahrs \cite{Kahrs-html,Kahrs-JFP01}. |
43 |
43 |
44 \paragraph{2-3 trees} |
44 \paragraph{2-3 trees} |
45 The function definitions are based on the teaching material by |
45 Equational definitions were given by Hoffmann and |
46 Turbak~\cite{Turbak230}. |
46 O'Donnell~\cite{HoffmannOD-TOPLAS82} (only insertion) |
|
47 and Reade \cite{Reade-SCP92}. |
|
48 Our formalisation is based on the teaching material by |
|
49 Turbak~\cite{Turbak230} . |
47 |
50 |
48 \paragraph{1-2 brother trees} |
51 \paragraph{1-2 brother trees} |
49 They were invented by Ottmann and Six~\cite{OttmannS76,OttmannW-CJ80}. |
52 They were invented by Ottmann and Six~\cite{OttmannS76,OttmannW-CJ80}. |
50 The functional version is due to Hinze~\cite{Hinze-bro12}. |
53 The functional version is due to Hinze~\cite{Hinze-bro12}. |
51 |
54 |