src/HOL/Data_Structures/document/root.tex
changeset 61203 a8a8eca85801
child 61224 759b5299a9f2
equal deleted inserted replaced
61202:9e37178084c5 61203:a8a8eca85801
       
     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}