\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{IDE: Introduction, Destruction, Elimination} 
\author{Mihails Milehins}
\maketitle

\newpage

\begin{abstract}
The document presents a reference manual for the
command \mbox{\textbf{mk\_ide}} developed 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}. 
The command provides means for the automated synthesis of the introduction,
destruction and elimination rules from the definitions of predicates stated
in Isabelle/HOL.
\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 
\href{https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users}
in the form of answers given to his general queries. 

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 
(especially Stack Overflow and TeX Stack Exchange) 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}