diff -r 78d828f43cdf -r 4b4742aa43f2 ESOP-Paper/document/root.tex
--- a/ESOP-Paper/document/root.tex	Sat Dec 17 16:58:11 2011 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,112 +0,0 @@
-\documentclass{llncs}
-\usepackage{times}
-\usepackage{isabelle}
-\usepackage{isabellesym}
-\usepackage{amsmath}
-\usepackage{amssymb}
-%%\usepackage{amsthm}
-\usepackage{tikz}
-\usepackage{pgf}
-\usepackage{pdfsetup}
-\usepackage{ot1patch}
-\usepackage{times}
-\usepackage{boxedminipage}
-\usepackage{proof}
-\usepackage{setspace}
-
-\allowdisplaybreaks
-\urlstyle{rm}
-\isabellestyle{it}
-\renewcommand{\isastyleminor}{\it}%
-\renewcommand{\isastyle}{\normalsize\it}%
-
-\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
-\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
-\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
-\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\hspace{-0.5mm}\cdot\hspace{-0.5mm}}$}}}
-\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
-\renewcommand{\isasymequiv}{$\dn$}
-%%\renewcommand{\isasymiota}{}
-\renewcommand{\isasymxi}{$..$}
-\renewcommand{\isasymemptyset}{$\varnothing$}
-\newcommand{\isasymnotapprox}{$\not\approx$}
-\newcommand{\isasymLET}{$\mathtt{let}$}
-\newcommand{\isasymAND}{$\mathtt{and}$}
-\newcommand{\isasymIN}{$\mathtt{in}$}
-\newcommand{\isasymEND}{$\mathtt{end}$}
-\newcommand{\isasymBIND}{$\mathtt{bind}$}
-\newcommand{\isasymANIL}{$\mathtt{anil}$}
-\newcommand{\isasymACONS}{$\mathtt{acons}$}
-\newcommand{\isasymCASE}{$\mathtt{case}$}
-\newcommand{\isasymOF}{$\mathtt{of}$}
-\newcommand{\isasymAL}{\makebox[0mm][l]{$^\alpha$}}
-\newcommand{\isasymPRIME}{\makebox[0mm][l]{$'$}}
-\newcommand{\isasymFRESH}{\#}
-\newcommand{\LET}{\;\mathtt{let}\;}
-\newcommand{\IN}{\;\mathtt{in}\;}
-\newcommand{\END}{\;\mathtt{end}\;}
-\newcommand{\AND}{\;\mathtt{and}\;}
-\newcommand{\fv}{\mathit{fv}}
-
-\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
-%----------------- theorem definitions ----------
-%%\theoremstyle{plain}
-%%\spnewtheorem{thm}[section]{Theorem}
-%%\newtheorem{property}[thm]{Property}
-%%\newtheorem{lemma}[thm]{Lemma}
-%%\spnewtheorem{defn}[theorem]{Definition}
-%%\spnewtheorem{exmple}[theorem]{Example}
-\spnewtheorem{myproperty}{Property}{\bfseries}{\rmfamily}
-%-------------------- environment definitions -----------------
-\newenvironment{proof-of}[1]{{\em Proof of #1:}}{}
-
-%\addtolength{\textwidth}{2mm}
-\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
-
-\begin{abstract} 
-Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
-prover. It provides a proving infrastructure for reasoning about
-programming language calculi involving named bound variables (as
-opposed to de-Bruijn indices). In this paper we present an extension of
-Nominal Isabelle for dealing with general bindings, that means
-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
-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
-
-
-\input{session}
-
-\begin{spacing}{0.9}
-  \bibliographystyle{plain}
-  \bibliography{root}
-\end{spacing}
-
-%\pagebreak
-%\input{Appendix} 
-
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End: