diff -r eab84ac2603b -r 5df574281b69 LMCS-Paper/document/root.tex
--- a/LMCS-Paper/document/root.tex	Mon Aug 15 17:42:35 2011 +0200
+++ b/LMCS-Paper/document/root.tex	Tue Aug 16 17:48:09 2011 +0200
@@ -1,5 +1,5 @@
-\documentclass{llncs}
-\usepackage{times}
+\documentclass{lmcs}
+%%\usepackage{times}
 \usepackage{isabelle}
 \usepackage{isabellesym}
 \usepackage{amsmath}
@@ -56,7 +56,7 @@
 %%\newtheorem{lemma}[thm]{Lemma}
 %%\spnewtheorem{defn}[theorem]{Definition}
 %%\spnewtheorem{exmple}[theorem]{Example}
-\spnewtheorem{myproperty}{Property}{\bfseries}{\rmfamily}
+%%\spnewtheorem{myproperty}{Property}{\bfseries}{\rmfamily}
 %-------------------- environment definitions -----------------
 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{}
 
@@ -64,11 +64,17 @@
 \addtolength{\parskip}{-0.33mm}
 \begin{document}
 
-\title{General Bindings and Alpha-Equivalence\\ in Nominal Isabelle}
-\author{Christian Urban and Cezary Kaliszyk}
-\institute{TU Munich, Germany}
-%%%{\{urbanc, kaliszyk\}@in.tum.de}
-\maketitle
+\title[Genral Bindings]{General Bindings and Alpha-Equivalence in Nominal Isabelle}
+\author{Christian Urban} 
+\address{Technical University of Munich, Germany}	
+\email{urbanc@in.tum.de}
+
+\author{Cezary Kaliszyk}
+\address{University of Tsukuba, Japan}
+\email{kaliszyk@score.cs.tsukuba.ac.jp}
+
+\keywords{Nominal Isabelle, variable convention, formal reasoning}
+\subjclass{MANDATORY list of acm classifications}
 
 \begin{abstract} 
 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
@@ -79,27 +85,18 @@
 term-constructors where multiple variables are bound at once. Such general
 bindings are ubiquitous in programming language research and only very
 poorly supported with single binders, such as lambda-abstractions. Our
-extension includes new definitions of $\alpha$-equivalence and establishes
-automatically the reasoning infrastructure for $\alpha$-equated terms. We
+extension includes new definitions of alpha-equivalence and establishes
+automatically the reasoning infrastructure for alpha-equated terms. We
 also prove strong induction principles that have the usual variable
 convention already built in.
 \end{abstract}
 
-%\category{F.4.1}{subcategory}{third-level}
-
-%\terms
-%formal reasoning, programming language calculi
-
-%\keywords
-%nominal logic work, variable convention
-
-
+\maketitle
 \input{session}
 
-\begin{spacing}{0.9}
-  \bibliographystyle{plain}
-  \bibliography{root}
-\end{spacing}
+\bibliographystyle{plain}
+\bibliography{root}
+
 
 %\pagebreak
 %\input{Appendix}