standardized towards new-style formal comments: isabelle update_comments;

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

isabelle update_cartouches -c -t;

prefer symbols;

renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'

adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
* * *
more transition of 'xxx_rec' to 'rec_xxx' and same for case
* * *
compile
* * *
'rename_tac's to avoid referring to generated names
* * *
more robust scripts with 'rename_tac'
* * *
'where' -> 'of'
* * *
'where' -> 'of'
* * *
renamed 'xxx_rec' to 'rec_xxx'

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

eliminated slightly odd identifiers;

tuned proofs;

Removed strange hack introduced in b27e93132603, since equivariance
is working again

explicitly spelt out proof of equivariance avoids problem with automation due to type constructor `set`

new fastforce replacing fastsimp - less confusing name

modernized specifications;

modernized primrec

repaired subscripts broken in d8d7d1b785af

replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)

Adapted to changes in induct method.

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

simplified proofs

deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means

Merge.

Added typing and evaluation relations, together with proofs of preservation
and progress (i.e. part 2A of the POPLmark challenge).

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

updated

Renamed inductive2 to inductive.

tuned proofs: avoid implicit prems;

nominal_inductive no longer proves equivariance.

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

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

adapted to nominal_inductive infrastructure

Adapted to new inductive definition package.

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

Adapted to new nominal_primrec command.

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

Adapted to changes in FCBs.

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

adapted using the characteristic equations

added definition for size and substitution using the recursion
combinator

added more infrastructure for the recursion combinator

Capitalized theory names.

no essential changes

cahges to use the new induction-principle (now proved in
full glory)

merged the silly lemmas into the eqvt proof of subtype

tuned

tuned

commented the transitivity and narrowing proof

added more documentation; will now try out a modification
of the ok-predicate

tuned more proofs

there was a small error in the last commit - fixed now

tuned more proof and added in-file documentation

tuned the proof of transitivity/narrowing

made further tunings

transitivity should be now in a reasonable state. But
Markus has to have a look at some of the advanced features.

started to change the transitivity/narrowing case:
have trouble with Q=Q.

changed everything until the interesting transitivity_narrowing
proof.

some small tuning

added an authors section (please let me know if somebody is left out or unhappy)

cleaned up all examples so that they work with the
current nominal-setting.

added fsub.thy (poplmark challenge) to the examples
directory.