session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;

isabelle update_cartouches -c -t;

standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;

Modified nominal_primrec to make it work with local theories, unified syntax
with the one used by fun(ction) and new version of primrec command.

made the naming of the induction principles consistent: weak_induct is
induct and induct is strong_induct

extended to be a library of general facts about the lambda calculus

tuned proofs and comments

deleted some unnecessary type-annotations

tuned some proofs and changed variable names in some definitions of Nominal.thy

adapted to new nominal_inductive

Unified function syntax

major update of the nominal package; there is now an infrastructure
for equivariance lemmas which eases definitions of nominal functions

added the function for free variables of a lambda-term, which is a
tad more difficult to define than capture-avoiding substitution

adapted function definitions to new syntax

more robust syntax for definition/abbreviation/notation;

new file for defining functions in the lambda-calculus