\documentclass[10pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{amssymb}
\usepackage[left=2.25cm,right=2.25cm,top=2.25cm,bottom=2.75cm]{geometry}
\usepackage{graphicx}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage{pdfsetup}

\urlstyle{tt}
\isabellestyle{it}

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}

\renewcommand{\isacharunderscore}{\_}

\begin{document}

\title{Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms}
\author{Alexander Bentkamp}

\maketitle

\begin{abstract}
\noindent
This Isabelle/HOL formalization defines the Embedding Path Order (EPO) for
higher-order terms without $\lambda$-abstraction and proves many useful
properties about it. In contrast to the lambda-free recursive path orders,
it does not fully coincide with RPO on first-order terms, but it is compatible
with arbitrary higher-order contexts.
\end{abstract}

\tableofcontents

% sane default for proof documents
\parindent 0pt
\parskip 0.5ex

\section{Introduction}

This Isabelle/HOL formalization defines the Embedding Path Order (EPO) for
higher-order terms without $\lambda$-abstraction and proves many useful
properties about it. In contrast to the lambda-free recursive path orders,
it does not fully coincide with RPO on first-order terms, but it is compatible
with arbitrary higher-order contexts.

% generated text of all theories
\input{session}

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

%\bibliographystyle{abbrv}
%\bibliography{bib}

\end{document}
