--- a/Quotient-Paper/document/root-sac.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{verbdef}
-\usepackage{longtable}
-\usepackage{mathpartir}
-\newtheorem{definition}{Definition}
-\newtheorem{proposition}{Proposition}
-\newtheorem{lemma}{Lemma}
-
-\urlstyle{rm}
-\isabellestyle{it}
-\renewcommand{\isastyleminor}{\it}%
-\renewcommand{\isastyle}{\normalsize\rm}%
-
-\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
-\verbdef\singlearr|--->|
-\verbdef\doublearr|===>|
-\verbdef\tripple|###|
-
-\renewcommand{\isasymequiv}{$\dn$}
-\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 Isabelle/HOL the quotient package by Homeier. In doing so we
-extended his work in order to deal with compositions of quotients. Like his
-package, we designed our quotient package so that every step in a quotient construction
-can be performed separately and as a result we are able to specify completely
-the procedure of lifting theorems from the raw level to the quotient level.
-The importance for programming language research is that many properties of
-programming language calculi are easier to verify over $\alpha$-equated, or
-$\alpha$-quotient, terms, than over raw terms.
-\end{abstract}
-
-\category{D.??}{TODO}{TODO}
-
-\keywords{quotients, isabelle, 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: