61203
|
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 |
|
61224
|
32 |
\setcounter{tocdepth}{1}
|
61203
|
33 |
\tableofcontents
|
|
34 |
\newpage
|
|
35 |
|
|
36 |
\input{session}
|
|
37 |
|
61224
|
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 |
\bibliographystyle{abbrv}
|
|
45 |
\bibliography{root}
|
61203
|
46 |
|
|
47 |
\end{document}
|