39 bla bla

    39 Nominal Isabelle provides an infrastructure for formal reasoning about terms

    40 involving named bound variables. This infrastructure allows bound variables to

    41 be analysed and manipulated directly. In this way it can mimic informal

    42 pen-and-pencil reasoning. However, this ability makes defining functions the

    43 most difficult aspect of the ``nominal approach''.  In this paper we present a

    44 new way of defining recursive functions over terms with bound variables.  For

    45 example, we are able to define without difficulties functions for CPS

    46 translations or the evaluation of lambda-terms, which were previously not

    47 definable in Nominal Isabelle. We also generalise the

    48 freshness-condition-for-binders to general binders recently introduced in

    49 Nominal Isabelle.