diff -r fb201e383f1b -r da575186d492 Quotient-Paper-jv/document/root.tex
--- a/Quotient-Paper-jv/document/root.tex	Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +0,0 @@
-\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: