--- a/Quotient-Paper/document/root-lncs.tex	Sat May 12 21:05:59 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-%\documentclass{svjour3}
-\documentclass{llncs}
-\usepackage{times}
-\usepackage{isabelle}
-\usepackage{isabellesym}
-\usepackage{amsmath}
-\usepackage{amssymb}
-\usepackage{pdfsetup}
-\usepackage{tikz}
-\usepackage{pgf}
-\usepackage{verbdef}
-\usepackage{longtable}
-\usepackage{mathpartir}
-
-\urlstyle{rm}
-\isabellestyle{it}
-\renewcommand{\isastyle}{\isastyleminor}
-
-\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}
-
-\title{Quotients Revisited for Isabelle/HOL}
-\author{Cezary Kaliszyk$^*$ and Christian Urban$^*$}
-\institute{$^*$ Technical University of Munich, Germany}
-\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}
-
-% generated text of all theories
-\input{session}
-
-% optional bibliography
-\bibliographystyle{abbrv}
-\bibliography{root}
-
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End: