\documentclass[11pt,a4paper]{report}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
\usepackage{pdfsetup}
\urlstyle{rm}
\isabellestyle{it}

\begin{document}

\title{Go Code Generation for Isabelle}
\author{Terru Stübinger, Lars Hupel}
\maketitle

\begin{abstract}
  This entry contains a standalone code generation target for the Go programming language.
  Unlike the previous targets, Go is not a functional language and encourages code in an imperative style, thus many of the features of Isabelle's language (particularly data types, pattern matching, and type classes) have to be emulated using imperative language constructs in Go.
  To generate Go code, users can simply import this entry, which makes the Go target available.
\end{abstract}

\parindent 0pt\parskip 0.5ex

\input{session}

\end{document}