\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 only+
−
mechanism for extension is the introduction of safe definitions and of+
−
non-empty types. Both extensions are often performed in quotient+
−
constructions. To ease the work involved with such quotient+
−
constructions, we re-implemented in the Isabelle/HOL theorem prover+
−
the quotient package by Homeier. In doing so we extended his work in+
−
order to deal with compositions of quotients and also specified+
−
completely the procedure of lifting theorems from the raw level to the+
−
quotient level.  The importance for theorem proving is that many+
−
formal verifications, in order to be feasible, require a convenient+
−
reasoning 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:+
−