--- a/Nominal/Ex/Exec/document/root.tex	Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,81 +0,0 @@
-\documentclass{llncs}
-\usepackage[utf8]{inputenc}
-\usepackage{lineno}
-\usepackage{url}
-\usepackage{amsmath,amssymb}
-\usepackage{isabelle,isabellesym}
-\usepackage{pdfsetup}
-\usepackage{ot1patch}
-%\usepackage{boxedminipage}
-
-\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.2mm}{\small$\bullet$}}}
-\renewcommand{\isasymintegral}{$\lambda$}
-\renewcommand{\isasymlbrace}{$\ulcorner$}
-\renewcommand{\isasymrbrace}{$\urcorner$}
-%\renewcommand{\isasymguillemotleft}{}
-%\renewcommand{\isasymguillemotright}{}
-
-\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
-\renewcommand{\isasymequiv}{=}
-%%\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}}
-\newenvironment{proof-of}[1]{{\em Proof of #1:}}{}
-
-\begin{document}
-
-\title{Execution modulo alpha-equivalence}
-\author{...\inst{1} \and ...\inst{2}}
-\institute{... \and ...}
-
-\maketitle
-
-\begin{abstract}
-  In this paper we show how a formal specification defined modulo
-  alpha-equivalence can be programatically made executable.
-  We show a general algorithm and we present examples of
-  executed calculi, which we implement in Nominal Isabelle.
-\end{abstract}
-
-\input{session}
-
-%\begin{spacing}{0.9}
-\bibliographystyle{abbrv}
-\bibliography{root}
-%\end{spacing}
-
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End: