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

isabelle update_cartouches -c -t;

more canonical names

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

Renamed inductive2 to inductive.

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

the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive

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

Adapted to new inductive definition package.

Adapted to new nominal_primrec command.

Adapted to changes in FCBs.

made some proof look more like the ones in Barendregt

this file contains a compile-challenge suggested by Adam Chlipala;
so far it contains only the definition and no proofs