\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}

\usepackage{pdfsetup}

\urlstyle{rm}
\isabellestyle{it}

\begin{document}

\title{Fixed-length vectors}
\author{Lars Hupel}

\maketitle

\begin{abstract}
This theory introduces a type constructor for lists with known length, also known as \emph{vectors}.
Those vectors are indexed with a numeral type that represent their length.
This can be employed to avoid carrying around length constraints on lists. Instead, those
constraints are discharged by the type checker.
As compared to the vectors defined in the distribution, this definition can easily work with unit
vectors. We exploit the fact that the cardinality of an infinite type is defined to be ‹0›: thus
any infinite length index type represents a unit vector.
Furthermore, we set up automation and BNF support.
\end{abstract}

\tableofcontents

\parindent 0pt\parskip 0.5ex

\input{session}

\end{document}