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

isabelle update_cartouches -c -t;

more canonical names

eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;

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

tuned

tuned proofs and comments

tuned proofs and comments

polishing of some proofs

further comments

polished the proofs and added a version of the weakening lemma that does not use the variable convention

added type constraints to resolve syntax ambiguities;

Renamed inductive2 to inductive.

nominal_inductive no longer proves equivariance.

tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts

adapted to new nominal_inductive infrastructure

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

added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user

fixed some typos

tuned the proof of the strong induction principle

added an intro lemma for freshness of products; set up
the simplifier so that it can deal with the compact and
long notation for freshness constraints (FIXME: it should
also be able to deal with the special case of freshness
of atoms)

more robust syntax for definition/abbreviation/notation;

replaced exists_fresh lemma with a version formulated with obtains;
old lemma is available as exists_fresh' (still needed in apply-scripts)

inductive2: canonical specification syntax;

new file for defining functions in the lambda-calculus

adapted to Stefan's new inductive package and cleaning up

made some proof look more like the ones in Barendregt

induct method: renamed 'fixing' to 'arbitrary';

added more infrastructure for the recursion combinator

Capitalized theory names.

tuned proofs

tuned the eqvt-proof

tuned

tuned

tuned

changed "fresh:" to "avoiding:" and cleaned up the weakening example

adapted to the new nominal_induction

some small tuning

Initial commit of the theory "Weakening".