--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quotient-Paper/document/root-lncs.tex	Fri Aug 27 13:57:00 2010 +0800
@@ -0,0 +1,69 @@
+%\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: