\documentclass[11pt,a4paper,parskip=half]{scrartcl}
\usepackage{isabelle,isabellesym}
\usepackage[only,bigsqcap]{stmaryrd}

% From src/HOL/HOLCF/document/root
\newcommand{\isasymnotsqsubseteq}{\isamath{\not\sqsubseteq}}

\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{tikz}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{mathpartir}
\usepackage{calc}

\usepackage{floatpag}
\floatpagestyle{empty}

% this should be the last package used
\usepackage{pdfsetup}

% silence the KOMA script warnings
\def\bf{\normalfont\bfseries}
\def\it{\normalfont\itshape}
\def\rm{\normalfont\rmfamily}


% urls in roman style, theorys in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

% Isabelle does not like *} in a text {* ... *} block
% Concrete implemenation thanks to http://www.mrunix.de/forums/showpost.php?p=235085&postcount=5
\newenvironment{alignstar}{\csname align*\endcsname}{\csname endalign*\endcsname}
\newenvironment{alignatstar}{\csname alignat*\endcsname}{\csname endalignat*\endcsname}

\DeclareUnicodeCharacter{00B2}{\ensuremath{^2}}

% Entering \ in Isabelle/jEdit has unwanted consequences
\catcode`\|=0 %

% From src/HOL/HOLCF/document/root
%\newcommand{\isasymnotsqsubseteq}{\isamath{\not\sqsubseteq}}


\begin{document}

\title{Lazy Evaluation:\\From natural semantics to a machine-checked compiler transformation}
\author{Joachim Breitner\\
Programming Paradigms Group\\
Karlsruhe Institute for Technology\\
\url{breitner@kit.edu}}
\maketitle

This document contains a rendering of the formal theories corresponding to doctorla thesis “Lazy Evaluation: From natural semantics to a machine-checked compiler transformation“ by Joachim Breitner. See \url{http://www.joachim-breitner.de/thesis} for more details.

These theories are also contained in the Archive of Formal Proofs; please see and cite \url{http://afp.sourceforge.net/entries/Launchbury.shtml} resp.\@ \url{http://afp.sourceforge.net/entries/Call_Arity.shtml}.

\tableofcontents

\let\OldSubsection\subsection
\let\OldSubsubsection\subsubsection
\renewcommand{\subsection}{\section}
\renewcommand{\subsubsection}{\OldSubsection}

\let\OldInput\input
\renewcommand{\input}[1]{{
        \section{#1}
        \OldInput{#1}
}}

\OldInput{session.tex}

\clearpage
\bibliographystyle{amsalpha}
\bibliography{root}

\end{document}