%\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 construction, 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:+
−