src/HOL/Data_Structures/document/root.tex
author nipkow
Wed Nov 18 10:12:37 2015 +0100 (2015-11-18)
changeset 61697 0753dd4c9144
parent 61525 87244a9cfe40
child 61784 21b34a2269e5
permissions -rw-r--r--
converted to cmp
     1 \documentclass[11pt,a4paper]{article}
     2 \usepackage{isabelle,isabellesym}
     3 \usepackage{latexsym}
     4 % this should be the last package used
     5 \usepackage{pdfsetup}
     6 
     7 % snip
     8 \newcommand{\repeatisanl}[1]{\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi}
     9 \newcommand{\snip}[4]{\repeatisanl#2#4\repeatisanl#3}
    10 
    11 \urlstyle{rm}
    12 \isabellestyle{it}
    13 
    14 \renewcommand{\isacharunderscore}{\_}
    15 \renewcommand{\isacharunderscorekeyword}{\_}
    16 
    17 % for uniform font size
    18 \renewcommand{\isastyle}{\isastyleminor}
    19 
    20 \begin{document}
    21 
    22 \title{Functional Data Structures}
    23 \author{Tobias Nipkow}
    24 \maketitle
    25 
    26 \begin{abstract}
    27 A collection of verified functional data structures. The emphasis is on
    28 conciseness of algorithms and succinctness of proofs, more in the style
    29 of a textbook than a library of efficient algorithms.
    30 \end{abstract}
    31 
    32 \setcounter{tocdepth}{1}
    33 \tableofcontents
    34 \newpage
    35 
    36 \input{session}
    37 
    38 \section{Bibliographic Notes}
    39 
    40 \paragraph{Red-black trees}
    41 The insert function follows Okasaki \cite{Okasaki}, the delete function
    42 Kahrs \cite{Kahrs-html,Kahrs-JFP01}.
    43 
    44 \paragraph{2-3 trees}
    45 The function definitions are based on the teaching material by
    46 Turbak~\cite{Turbak230}.
    47 
    48 \paragraph{Splay trees}
    49 They were invented by Sleator and Tarjan \cite{SleatorT-JACM85}.
    50 Our formalisation follows Schoenmakers \cite{Schoenmakers-IPL93}.
    51 
    52 \bibliographystyle{abbrv}
    53 \bibliography{root}
    54 
    55 \end{document}