diff -r a6f3e1b08494 -r b6873d123f9b LMCS-Paper/document/root.tex
--- a/LMCS-Paper/document/root.tex	Sat May 12 21:05:59 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,112 +0,0 @@
-\documentclass{lmcs}
-%%\usepackage{times}
-\usepackage{isabelle}
-\usepackage{isabellesym}
-\usepackage{amsmath}
-\usepackage{amssymb}
-%%\usepackage{amsthm}
-\usepackage{tikz}
-\usepackage{pgf}
-\usepackage{ot1patch}
-\usepackage{times}
-\usepackage{boxedminipage}
-\usepackage{proof}
-\usepackage{setspace}
-\usepackage{afterpage}
-\usepackage{pdfsetup}
-
-\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[Genral Bindings]{General Bindings and Alpha-Equivalence in Nominal
-Isabelle$^\star$}
-\author{Christian Urban} 
-\address{King's College London, United Kingdom}	
-\email{christian.urban@kcl.ac.uk}
-
-\author{Cezary Kaliszyk}
-\address{University of Innsbruck, Austria}
-\email{cezary.kaliszyk@uibk.ac.at}
-\thanks{$^\star$~This is a revised and expanded version of~\cite{UrbanKaliszyk11}}
-
-\keywords{Nominal Isabelle, variable convention, alpha-equivalence, theorem provers, formal reasoning, lambda-calculus}
-\subjclass{F.3.1}
-
-\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}
-
-\maketitle
-\input{session}
-
-\bibliographystyle{plain}
-\bibliography{root}
-
-
-%\pagebreak
-%\input{Appendix} 
-
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End: