\documentclass{sig-alternate}
  \pdfpagewidth=8.5truein
  \pdfpageheight=11truein
\usepackage{times}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{pdfsetup}
\usepackage{tikz}
\usepackage{pgf}
\usepackage{verbdef}
\usepackage{longtable}
\usepackage{mathpartir}
\newtheorem{definition}{Definition}
\newtheorem{proposition}{Proposition}
\newtheorem{lemma}{Lemma}

\urlstyle{rm}
\isabellestyle{rm}
\renewcommand{\isastyleminor}{\rm}%
\renewcommand{\isastyle}{\normalsize\rm}%

\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
\verbdef\singlearr|--->|
\verbdef\doublearr|===>|
\verbdef\tripple|###|

\renewcommand{\isasymequiv}{$\triangleq$}
\renewcommand{\isasymemptyset}{$\varnothing$}
%%\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
\renewcommand{\isasymUnion}{$\bigcup$}

\newcommand{\isasymsinglearr}{\singlearr}
\newcommand{\isasymdoublearr}{\doublearr}
\newcommand{\isasymtripple}{\tripple}

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

\begin{document}

\conferenceinfo{SAC'11}{March 21-25, 2011, TaiChung, Taiwan.}
\CopyrightYear{2011}
\crdata{978-1-4503-0113-8/11/03}

\title{Quotients Revisited for Isabelle/HOL}
\numberofauthors{2}
\author{
\alignauthor
Cezary Kaliszyk\\
  \affaddr{University of Tsukuba, Japan}\\
  \email{kaliszyk@score.cs.tsukuba.ac.jp}
\alignauthor
Christian Urban\\
  \affaddr{Technical University of Munich, Germany}\\
  \email{urbanc@in.tum.de}
}

\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 popular 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 we are also able to specify 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 resoning infrastructure 
for quotient constructions.
\end{abstract}

%\category{D.??}{TODO}{TODO}

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

% generated text of all theories
\input{session}

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: