--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quotient-Paper-jv/document/root.tex	Tue Dec 20 17:54:53 2011 +0900
@@ -0,0 +1,76 @@
+\documentclass{svjour3}
+\usepackage{times}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{pdfsetup}
+\usepackage{tikz}
+%\usepackage{pgf}
+\usepackage{stmaryrd}
+\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}%
+\renewcommand{\isastylescript}{\it}
+\def\dn{\,\triangleq\,}
+\verbdef\singlearr|---->|
+\verbdef\doublearr|===>|
+\verbdef\tripple|###|
+
+\renewcommand{\isasymequiv}{$\triangleq$}
+\renewcommand{\isasymemptyset}{$\varnothing$}
+%%\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+\renewcommand{\isasymUnion}{$\bigcup$}
+
+\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 Tsukuba, Japan
+     \and C.~Urban \at Technical University of Munich, Germany}
+\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 %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 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: