\documentclass[11pt,a4paper]{article}

 \usepackage[latin1]{inputenc}

 \usepackage{isabelle,isabellesym}

 \usepackage{pdfsetup}

 \urlstyle{rm}

 % pretty printing for the Com language

 %\newcommand{\CMD}[1]{\isatext{\bf\sffamily#1}}

 \newcommand{\CMD}[1]{\isatext{\rm\sffamily#1}}

 \newcommand{\isasymSKIP}{\CMD{skip}}

 \newcommand{\isasymIF}{\CMD{if}}

 \newcommand{\isasymTHEN}{\CMD{then}}

 \newcommand{\isasymELSE}{\CMD{else}}

 \newcommand{\isasymWHILE}{\CMD{while}}

 \newcommand{\isasymDO}{\CMD{do}}

 \addtolength{\hoffset}{-1cm}

 \addtolength{\textwidth}{2cm}

 \begin{document}

 \title{IMP in HOLCF}

 \author{Tobias Nipkow and Robert Sandner}

 \maketitle

 \tableofcontents

 \parindent 0pt\parskip 0.5ex

 \input{session}

 \bibliographystyle{abbrv}

 \bibliography{root}

 \end{document}