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


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

\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
\renewcommand{\isasymequiv}{$\dn$}
\renewcommand{\isasymemptyset}{$\varnothing$}

\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), used in several theorem provers, is based on a 
small logic kernel, whose only mechanism for extension is the introduction 
of safe definitions and non-empty 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. The importance to programming language research
is that many properties of programming languages are more convenient to verify
over $\alpha$-quotient terms, than over raw terms.
\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: