1\documentclass[11pt,a4paper]{article} 2\usepackage{isabelle,isabellesym} 3\usepackage{pdfsetup} 4 5\urlstyle{rm} 6\isabellestyle{it} 7 8\begin{document} 9 10\title{Examples for program extraction in Higher-Order Logic} 11\author{Stefan Berghofer} 12\maketitle 13 14\nocite{Berger-JAR-2001,Coquand93} 15 16\tableofcontents 17 18\parindent 0pt\parskip 0.5ex 19 20\input{session} 21 22\bibliographystyle{abbrv} 23\bibliography{root} 24 25\end{document} 26