%\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 a number of 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 and as a
result were able to specify completely the procedure of lifting theorems from
the raw level to the quotient level.  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: