--- a/Quotient-Paper/document/root.tex	Sat Dec 17 16:58:11 2011 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,92 +0,0 @@
-\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{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}
-
-\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@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 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}
-
-%\category{D.??}{TODO}{TODO}
-
-\keywords{Quotients, Isabelle theorem prover, Higher-Order Logic}
-
-% generated text of all theories
-\bibliographystyle{abbrv}
-\input{session}
-
-
-
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End: