src/HOL/Data_Structures/document/root.tex
author nipkow
Mon Sep 21 14:44:32 2015 +0200 (2015-09-21)
changeset 61203 a8a8eca85801
child 61224 759b5299a9f2
permissions -rw-r--r--
New subdirectory for functional data structures
     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}{2}
    33 \tableofcontents
    34 \newpage
    35 
    36 % generated text of all theories
    37 \input{session}
    38 
    39 %\bibliographystyle{abbrv}
    40 %\bibliography{root}
    41 
    42 \end{document}