isabelle update -u control_cartouches;

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

isabelle update_cartouches -c -t;

tuned proofs -- clarified flow of facts wrt. calculation;

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

tuned proofs;

modernized specifications;

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

tuned some proofs

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.

more function -> fun

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

removed test artefacts

avoid duplicate fact bindings;

tuned proofs: avoid implicit prems;

added type constraints to resolve syntax ambiguities;

undo a change in last commit : give a single name to the inversion lemmas for the same inductive type

updated some of the definitions and proofs

Renamed inductive2 to inductive.

fine tune automatic generation of inversion lemmas

tuned proofs: avoid implicit prems;

added the Q_Unit rule (was missing) and adjusted the proof accordingly

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

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

perm_simp can now simplify using the rules (a,b) o a = b and (a,b) o b = a

add a few details in the Fst and Snd cases of unicity proof

- Renamed <predicate>_eqvt to <predicate>.eqvt
- Renamed induct_weak to weak_induct

tuned proofs (taking full advantage of nominal_inductive)

Adapted to changes in nominal_inductive.

fixed function syntax

tuned some proofs

Unified function syntax

correct typo in latex output

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

tuned a bit the proofs

formalisation of Crary's chapter on logical relations
(in the book on Advanced Topics in Type Systems) done
by Narboux and Urban