\documentclass{svjour3}\usepackage{amsmath}\usepackage{amssymb}\usepackage{isabelle}\usepackage{isabellesym}\usepackage{tikz}\usepackage{verbdef}\usepackage{mathpartir}\usepackage{pdfsetup}\usepackage{times}\usepackage{stmaryrd}\urlstyle{rm}\isabellestyle{it}\renewcommand{\isastyleminor}{\it}%\renewcommand{\isastyle}{\normalsize\it}%\renewcommand{\isastylescript}{\it}\def\dn{\,\triangleq\,}\verbdef\singlearr|---->|\verbdef\doublearr|===>|\verbdef\tripple|###|\renewcommand{\isasymequiv}{$\triangleq$}\renewcommand{\isasymemptyset}{$\varnothing$}\renewcommand{\isasymUnion}{$\bigcup$}\renewcommand{\isacharunderscore}{\text{$\_\!\_$}}\newcommand{\isasymsinglearr}{$\mapsto$}\newcommand{\isasymdoublearr}{$\Mapsto$}\newcommand{\isasymtripple}{\tripple}\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}\begin{document}\title{Quotients Revisited for Isabelle/HOL}\author{Cezary Kaliszyk \and Christian Urban}\institute{C.~Kaliszyk \at University of Innsbruck, Austria \and C.~Urban \at King's College London, UK}\date{Received: date / Accepted: date}\maketitle\begin{abstract}Higher-Order Logic (HOL) is based on a small logic kernel, whose onlymechanism for extension is the introduction of safe definitions and ofnon-empty types. Both extensions are often performed in quotientconstructions. To ease the work involved with such quotientconstructions, we re-implemented in the Isabelle/HOL theorem proverthe quotient package by Homeier. In doing so we extended his work inorder to deal with compositions of quotients and also specifiedcompletely the procedure of lifting theorems from the raw level to thequotient level. The importance for theorem proving is that manyformal verifications, in order to be feasible, require a convenientreasoning infrastructure for quotient constructions.\end{abstract}%\keywords{Quotients, Isabelle theorem prover, Higher-Order Logic}\bibliographystyle{abbrv}\input{session}\end{document}%%% Local Variables:%%% mode: latex%%% TeX-master: t%%% End: