--- a/Fun-Paper/document/root.tex	Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,71 +0,0 @@
-\documentclass[preprint]{sigplanconf}
-\usepackage{isabelle}
-\usepackage{isabellesym}
-\usepackage{amsmath}
-\usepackage{amssymb}
-\usepackage{pdfsetup}
-\usepackage{ot1patch}
-\usepackage{times}
-\usepackage{stmaryrd}
-
-\urlstyle{rm}
-\isabellestyle{it}
-\renewcommand{\isastyleminor}{\it}%
-\renewcommand{\isastyle}{\normalsize\it}%
-
-
-\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
-\renewcommand{\isasymequiv}{$\dn$}
-\renewcommand{\isasymemptyset}{$\varnothing$}
-\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
-
-\newcommand{\isasymcalL}{\ensuremath{\cal{L}}}
-\newcommand{\isasymbigplus}{\ensuremath{\bigplus}}
-
-\newcommand{\bigplus}{\mbox{\Large\bf$+$}}
-\begin{document}
-
-%\titlebanner{Nominal Functions}      % These are ignored unless
-%\preprintfooter{Nominal Functions}   % 'preprint' option specified.
-
-\title{Nominal Functions}
-\authorinfo{?}
-           {?}
-           {?}
-
-\maketitle
-
-\begin{abstract} 
-Nominal Isabelle provides an infrastructure for formal reasoning about terms
-involving named bound variables. This infrastructure allows bound variables to
-be analysed and manipulated directly. In this way it can mimic informal
-pen-and-pencil reasoning. However, this ability makes defining functions the
-most difficult aspect of the ``nominal approach''.  In this paper we present a
-new way of defining recursive functions over terms with bound variables.  For
-example, we are able to define without difficulties functions for CPS
-translations or the evaluation of lambda-terms, which were previously not
-definable in Nominal Isabelle. We also generalise the
-freshness-condition-for-binders to general binders recently introduced in
-Nominal Isabelle.
-\end{abstract}
-
-\category{CR-number}{subcategory}{third-level}
-
-\terms
-term1, term2
-
-\keywords
-keyword1, keyword2
-
-
-\input{session}
-
-%\bibliographystyle{plain}
-%\bibliography{root}
-
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End: