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

isabelle update_cartouches -c -t;

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

removed duplicate lemmas;

tuned

tuned proofs and comments

tuned proofs: avoid implicit prems;

tuned Proof

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

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

adapted function definitions to new syntax

Adapted to changes in FCBs.

cleaning up

modified to use the characteristic equations

used the recursion combinator for the height and substitution function

added an example suggested by D. Wang on the PoplMark-mailing list;
it shows how the height of an alpha-equated lambda term interacts
with capture-avoiding substitution