--- a/Paper/document/root.tex	Fri Oct 01 07:11:47 2010 -0400
+++ b/Paper/document/root.tex	Mon Oct 04 07:25:37 2010 +0100
@@ -1,9 +1,9 @@
-\documentclass{sigplanconf}
+\documentclass{llncs}
 \usepackage{isabelle}
 \usepackage{isabellesym}
 \usepackage{amsmath}
 \usepackage{amssymb}
-\usepackage{amsthm}
+%%\usepackage{amsthm}
 \usepackage{tikz}
 \usepackage{pgf}
 \usepackage{pdfsetup}
@@ -47,12 +47,12 @@
 
 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
 %----------------- theorem definitions ----------
-\theoremstyle{plain}
-\newtheorem{thm}{Theorem}[section]
-\newtheorem{property}[thm]{Property}
-\newtheorem{lemma}[thm]{Lemma}
-\newtheorem{defn}[thm]{Definition}
-\newtheorem{exmple}[thm]{Example}
+%%\theoremstyle{plain}
+%%\spnewtheorem{thm}[section]{Theorem}
+%%\newtheorem{property}[thm]{Property}
+%%\newtheorem{lemma}[thm]{Lemma}
+%%\spnewtheorem{defn}[theorem]{Definition}
+%%\spnewtheorem{exmple}[theorem]{Example}
 
 %-------------------- environment definitions -----------------
 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{}
@@ -60,10 +60,10 @@
 
 \begin{document}
 
-\title{\LARGE\bf General Bindings and Alpha-Equivalence in Nominal Isabelle}
-\authorinfo{Christian Urban and Cezary Kaliszyk}
-           {TU Munich, Germany}
-           {\{urbanc, kaliszyk\}@in.tum.de}
+\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
 
 \begin{abstract} 
@@ -84,11 +84,11 @@
 
 %\category{F.4.1}{subcategory}{third-level}
 
-\terms
-formal reasoning, programming language calculi
+%\terms
+%formal reasoning, programming language calculi
 
-\keywords
-nominal logic work, variable convention
+%\keywords
+%nominal logic work, variable convention
 
 
 \input{session}