1 \documentclass{svjour3}

     2 \usepackage{amsmath}

     3 \usepackage{amssymb}

     4 \usepackage{isabelle}

     5 \usepackage{isabellesym}

     6 \usepackage{tikz}

     7 \usepackage{verbdef}

     8 \usepackage{mathpartir}

     9 \usepackage{pdfsetup}

    10 \usepackage{times}

    11 \usepackage{stmaryrd}

    12 

    13 \urlstyle{rm}

    14 \isabellestyle{it}

    15 \renewcommand{\isastyleminor}{\it}%

    16 \renewcommand{\isastyle}{\normalsize\it}%

    17 \renewcommand{\isastylescript}{\it}

    18 \def\dn{\,\triangleq\,}

    19 \verbdef\singlearr|---->|

    20 \verbdef\doublearr|===>|

    21 \verbdef\tripple|###|

    22 

    23 \renewcommand{\isasymequiv}{$\triangleq$}

    24 \renewcommand{\isasymemptyset}{$\varnothing$}

    25 \renewcommand{\isasymUnion}{$\bigcup$}

    26 \renewcommand{\isacharunderscore}{\text{$\_\!\_$}}

    27 

    28 \newcommand{\isasymsinglearr}{$\mapsto$}

    29 \newcommand{\isasymdoublearr}{$\Mapsto$}

    30 \newcommand{\isasymtripple}{\tripple}

    31 

    32 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}

    33 

    34 \begin{document}

    35 

    36 \title{Quotients Revisited for Isabelle/HOL}

    37 \author{Cezary Kaliszyk \and Christian Urban}

    38 \institute{C.~Kaliszyk \at University of Innsbruck, Austria

    39       \and C.~Urban \at King's College London, UK}

    40 \date{Received: date / Accepted: date}

    41 

    42 \maketitle

    43 

    44 \begin{abstract}

    45 Higher-Order Logic (HOL) is based on a small logic kernel, whose only

    46 mechanism for extension is the introduction of safe definitions and of

    47 non-empty types. Both extensions are often performed in quotient

    48 constructions. To ease the work involved with such quotient

    49 constructions, we re-implemented in the Isabelle/HOL theorem prover

    50 the quotient package by Homeier. In doing so we extended his work in

    51 order to deal with compositions of quotients and also specified

    52 completely the procedure of lifting theorems from the raw level to the

    53 quotient level.  The importance for theorem proving is that many

    54 formal verifications, in order to be feasible, require a convenient

    55 reasoning infrastructure for quotient constructions.

    56 \end{abstract}

    57 

    58 %\keywords{Quotients, Isabelle theorem prover, Higher-Order Logic}

    59 

    60 \bibliographystyle{abbrv}

    61 \input{session}

    62 

    63 

    64 

    65 \end{document}

    66 

    67 %%% Local Variables:

    68 %%% mode: latex

    69 %%% TeX-master: t

    70 %%% End: