\PassOptionsToPackage{ngerman,main=english}{babel}
\documentclass[11pt,a4paper]{article}
\usepackage{iman,extra,isar}
\usepackage{isabelle,isabellesym}
\usepackage{railsetup}

\usepackage[margin={1in,1in}]{geometry}

\usepackage[T1]{fontenc} 
\usepackage{lmodern}
\usepackage{babel}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{xspace}
\usepackage{MnSymbol}
\usepackage[utf8]{inputenc}
\usepackage{enumitem}
\usepackage{fontspec}

\usepackage{graphicx}
\usepackage{proof}

% bibliography
\usepackage[nottoc]{tocbibind}
\usepackage[square,numbers]{natbib}
\bibliographystyle{abbrvnat}

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

% drop Isabelle tags
\isadroptag{theory}

% enumitem configuration
\setlist{noitemsep,topsep=0pt,parsep=0pt,partopsep=0pt}

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

\begin{document}
\sloppy

\title{Conditional Transfer Rule: Reference Manual} 
\author{Mihails Milehins}
\maketitle

\newpage

\begin{abstract}
The document presents a reference manual for the framework 
\textit{Conditional Transfer Rule}: a collection of experimental utilities 
for \textit{unoverloading} 
\cite{kaufmann_mechanized_2010} 
of definitions and synthesis 
of \textit{conditional transfer rules} \cite{gonthier_lifting_2013}
for the object logic \textit{Isabelle/HOL} 
(e.g., see \cite{yang_comprehending_2017}) 
of the formal proof assistant \textit{Isabelle} \cite{paulson_natural_1986} 
written in \textit{Isabelle/ML} 
\cite{milner_definition_1997, wenzel_isabelle/isar_2019}. 
\end{abstract}

\newpage

\renewcommand{\abstractname}{Acknowledgements}
\begin{abstract}

The author would like to acknowledge the assistance that he received from 
the users of the mailing list of Isabelle 
\cite{noauthor_isabelle_nodate}
in the form of answers given to his general queries. 
Special thanks go to Fabian Immler for the development and implementation 
of the original algorithm for unoverloading of definitions 
\cite{immler_automation_2019}, for suggesting the original idea for 
the implementation of a framework for the relativization of definitions
(the idea evolved from \cite{immler_smooth_2019}) and for providing 
an outline of the first feasible algorithm for this task (implemented as 
\textit{CTR II}), 
to Andrei Popescu for trying the software and providing feedback, 
to Kevin Kappelmann for providing an explanation of certain aspects of 
\cite{kappelmann_speccheck_2021},
to Alexander Krauss for providing an explanation of certain aspects of 
\cite{kaufmann_mechanized_2010}, 
to Andreas Lochbihler for providing an outline 
of an improved algorithm for the relativization of definitions 
(not currently implemented), to Andreas Lochbihler and Dmitriy Traytel 
for providing an explanation of the existing functionality of the framework 
Conditional Parametricity \cite{gilcher_conditional_2017}.   
Furthermore, the author would like to acknowledge the positive 
impact of \cite{urban_isabelle_2019} and 
\cite{wenzel_isabelle/isar_2019} on his ability to code in Isabelle/ML.
Moreover, the author would like to acknowledge
the positive role that numerous Q\&A posted on the Stack Exchange network 
\cite{noauthor_stack_nodate} played in the development of this work. 
The author would also like to express gratitude to all members of his family 
and friends for their continuous support.

\end{abstract}

\newpage

\tableofcontents

\newpage

\parindent 0pt\parskip 0.5ex

\input{session}

\newpage

\bibliography{root}

\end{document}