%\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}

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: