src/HOLCF/IMP/document/root.tex
changeset 40774 0437dbc127b3
parent 40773 6c12f5e24e34
child 40775 ed7a4eadb2f6
equal deleted inserted replaced
40773:6c12f5e24e34 40774:0437dbc127b3
     1 
       
     2 \documentclass[11pt,a4paper]{article}
       
     3 \usepackage[latin1]{inputenc}
       
     4 \usepackage{isabelle,isabellesym}
       
     5 \usepackage{pdfsetup}
       
     6 
       
     7 \urlstyle{rm}
       
     8 
       
     9 % pretty printing for the Com language
       
    10 %\newcommand{\CMD}[1]{\isatext{\bf\sffamily#1}}
       
    11 \newcommand{\CMD}[1]{\isatext{\rm\sffamily#1}}
       
    12 \newcommand{\isasymSKIP}{\CMD{skip}}
       
    13 \newcommand{\isasymIF}{\CMD{if}}
       
    14 \newcommand{\isasymTHEN}{\CMD{then}}
       
    15 \newcommand{\isasymELSE}{\CMD{else}}
       
    16 \newcommand{\isasymWHILE}{\CMD{while}}
       
    17 \newcommand{\isasymDO}{\CMD{do}}
       
    18 
       
    19 \addtolength{\hoffset}{-1cm}
       
    20 \addtolength{\textwidth}{2cm}
       
    21 
       
    22 \begin{document}
       
    23 
       
    24 \title{IMP in HOLCF}
       
    25 \author{Tobias Nipkow and Robert Sandner}
       
    26 \maketitle
       
    27 
       
    28 \tableofcontents
       
    29 
       
    30 \parindent 0pt\parskip 0.5ex
       
    31 \input{session}
       
    32 
       
    33 \bibliographystyle{abbrv}
       
    34 \bibliography{root}
       
    35 
       
    36 \end{document}