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

\begin{document}

\title{Lazifying case constants}
\author{Lars Hupel}
\maketitle

\begin{abstract}
  Isabelle's code generator performs various adaptations for target languages. Among others,
  case statements are printed as match expressions. Internally, this is a sophisticated procedure,
  because in HOL, case statements are represented as nested calls to the case combinators as
  generated by the datatype package. Furthermore, the procedure relies on laziness of match
  expressions in the target language, i.e., that branches guarded by patterns that fail to match are
  not evaluated. Similarly, \texttt{if-then-else} is printed to the corresponding construct in the
  target language. This entry provides tooling to replace these special cases in the code generator
  by ignoring these target language features, instead printing case expressions and
  \texttt{if-then-else} as functions.
\end{abstract}

\parindent 0pt\parskip 0.5ex

\input{session}

% optional bibliography
%\bibliographystyle{abbrv}
%\bibliography{root}

\end{document}