%\documentclass{svjour3}
\documentclass{llncs}
\usepackage{times}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{pdfsetup}


\urlstyle{rm}
\isabellestyle{it}
\renewcommand{\isastyle}{\isastyleminor}

\begin{document}

\title{Quotients Revisited for Isabelle/HOL}
\author{Cezary Kaliszyk$^*$ and Christian Urban$^*$}
\institute{$^*$ Technical University of Munich, Germany}
\maketitle

\begin{abstract}
Higher-order logic (HOL) is based on a small logic kernel, whose 
only mechanism for extension is the introduction of definitions 
and types. Both extensions are often performed by 
quotient constructions, for example finite sets are constructed by quotienting
lists, or integers by quotienting pairs of natural numbers. To ease the work 
involved with quotient constructions, we re-implemented in Isabelle/HOL
the quotient package by Homeier. In doing so we extended his work 
in order to deal with compositions of quotients. Also, we designed
our quotient package so that every step in a quotient construction 
can be performed separately. 
\end{abstract}

% generated text of all theories
\input{session}

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

\end{document}

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