except for the interated binder case, finished definition in Calssical.thy
\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 termsinvolving named bound variables. This infrastructure allows bound variables tobe analysed and manipulated directly. In this way it can mimic informalpen-and-pencil reasoning. However, this ability makes defining functions themost difficult aspect of the ``nominal approach''. In this paper we present anew way of defining recursive functions over terms with bound variables. Forexample, we are able to define without difficulties functions for CPStranslations or the evaluation of lambda-terms, which were previously notdefinable in Nominal Isabelle. We also generalise thefreshness-condition-for-binders to general binders recently introduced inNominal Isabelle.\end{abstract}\category{CR-number}{subcategory}{third-level}\termsterm1, term2\keywordskeyword1, keyword2\input{session}%\bibliographystyle{plain}%\bibliography{root}\end{document}%%% Local Variables:%%% mode: latex%%% TeX-master: t%%% End: