\documentclass{svjour3}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{tikz}
\usepackage{verbdef}
\usepackage{mathpartir}
\usepackage{pdfsetup}
\usepackage{times}
\usepackage{stmaryrd}

\urlstyle{rm}
\isabellestyle{it}
\renewcommand{\isastyleminor}{\it}%
\renewcommand{\isastyle}{\normalsize\it}%
\renewcommand{\isastylescript}{\it}
\def\dn{\,\triangleq\,}
\verbdef\singlearr|---->|
\verbdef\doublearr|===>|
\verbdef\tripple|###|

\renewcommand{\isasymequiv}{$\triangleq$}
\renewcommand{\isasymemptyset}{$\varnothing$}
\renewcommand{\isasymUnion}{$\bigcup$}
\renewcommand{\isacharunderscore}{\text{$\_\!\_$}}

\newcommand{\isasymsinglearr}{$\mapsto$}
\newcommand{\isasymdoublearr}{$\Mapsto$}
\newcommand{\isasymtripple}{\tripple}

\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}

\begin{document}

\title{Quotients Revisited for Isabelle/HOL}
\author{Cezary Kaliszyk \and Christian Urban}
\institute{C.~Kaliszyk \at University of Innsbruck, Austria
      \and C.~Urban \at King's College London, UK}
\date{Received: date / Accepted: date}

\maketitle

\begin{abstract}
Higher-Order Logic (HOL) is based on a small logic kernel, whose only
mechanism for extension is the introduction of safe definitions and of
non-empty types. Both extensions are often performed in quotient
constructions. To ease the work involved with such quotient
constructions, we re-implemented in the Isabelle/HOL theorem prover
the quotient package by Homeier. In doing so we extended his work in
order to deal with compositions of quotients and also specified
completely the procedure of lifting theorems from the raw level to the
quotient level.  The importance for theorem proving is that many
formal verifications, in order to be feasible, require a convenient
reasoning infrastructure for quotient constructions.
\end{abstract}

%\keywords{Quotients, Isabelle theorem prover, Higher-Order Logic}

\bibliographystyle{abbrv}
\input{session}



\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: