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