--- a/Quotient-Paper/document/root.tex	Fri Aug 27 02:25:40 2010 +0000
+++ b/Quotient-Paper/document/root.tex	Fri Aug 27 13:57:00 2010 +0800
@@ -1,5 +1,6 @@
-%\documentclass{svjour3}
-\documentclass{llncs}
+\documentclass{sig-alternate}
+  \pdfpagewidth=8.5truein
+  \pdfpageheight=11truein
 \usepackage{times}
 \usepackage{isabelle}
 \usepackage{isabellesym}
@@ -11,10 +12,14 @@
 \usepackage{verbdef}
 \usepackage{longtable}
 \usepackage{mathpartir}
+\newtheorem{definition}{Definition}
+\newtheorem{proposition}{Proposition}
+\newtheorem{lemma}{Lemma}
 
 \urlstyle{rm}
 \isabellestyle{it}
-\renewcommand{\isastyle}{\isastyleminor}
+\renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastyle}{\normalsize\rm}%
 
 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
 \verbdef\singlearr|--->|
@@ -34,9 +39,23 @@
 
 \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}
-\author{Cezary Kaliszyk$^*$ and Christian Urban$^*$}
-\institute{$^*$ Technical University of Munich, Germany}
+\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}
@@ -54,6 +73,10 @@
 $\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}