src/HOL/Data_Structures/document/root.tex
changeset 61791 21502fb1ff0a
parent 61784 21b34a2269e5
child 62496 f187aaf602c4
     1.1 --- a/src/HOL/Data_Structures/document/root.tex	Sat Dec 05 16:33:20 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/document/root.tex	Sat Dec 05 17:23:50 2015 +0100
     1.3 @@ -42,8 +42,11 @@
     1.4  Kahrs \cite{Kahrs-html,Kahrs-JFP01}.
     1.5  
     1.6  \paragraph{2-3 trees}
     1.7 -The function definitions are based on the teaching material by
     1.8 -Turbak~\cite{Turbak230}.
     1.9 +Equational definitions were given by Hoffmann and
    1.10 +O'Donnell~\cite{HoffmannOD-TOPLAS82} (only insertion)
    1.11 +and Reade \cite{Reade-SCP92}.
    1.12 +Our formalisation is based on the teaching material by
    1.13 +Turbak~\cite{Turbak230} .
    1.14  
    1.15  \paragraph{1-2 brother trees}
    1.16  They were invented by Ottmann and Six~\cite{OttmannS76,OttmannW-CJ80}.