made sure the raw datatypes and raw functions do not get any mixfix syntax

exported the code into a separate file

strong rule inductions; as an example the weakening lemma works

final version of the ESOP paper; used set+ instead of res as requested by one reviewer

file with most of the strong rule induction development

simple cases for string rule inductions

changed res keyword to set+ for restrictions; comment by a referee

added proper case names for all induct and exhaust theorems

added small example for strong inductions; functions still need a sorry

removed local fix for bug in induction_schema; added setup method for strong inductions

automated all strong induction lemmas

proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML

generated goals for strong induction theorems.

test with strong inductions

moved all strong_exhaust code to nominal_dt_quot; tuned examples

moved generic functions into nominal_library

slight tuning

slight tuning

tuned examples

added fold_right which produces the correct term for left-infix operators

updated to Isabelle 22 December

a bit tuning

corrected premises of strong exhausts theorems

properly exported strong exhaust theorem; cleaned up some examples

all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code

one interesting case done

a stronger statement for at_set_avoiding

tuned

tuned

simple cases for strong inducts done; infrastructure for the difficult ones is there

added theorem-rewriter conversion

freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through)

created strong_exhausts terms

moved setify and listify functions into the library; introduced versions that have a type argument

updated

a bit more tuning of the paper

brought the paper to 20 pages plus one page appendix

first tests about exhaust

moved some code into the nominal_library

moved definition of raw bn-functions into nominal_dt_rawfuns

kept the nested structure of constructors (belonging to one datatype)

moved general theorems into the libraries

automated permute_bn theorems

updated to changes in Isabelle

deleted nominal_dt_supp.ML

moved code from nominal_dt_supp to nominal_dt_quot

automated alpha_perm_bn theorems

ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof

updated to Isabelle 2nd December

isarfied some of the high-level proofs

added abs_rename_res lemma

completed proofs in Foo2

completed the strong exhausts rules for Foo2 using general lemmas

tuned proof to reduce number of warnings

disabled the Foo examples, because of heavy work

slightly simplified the Foo2 tests and hint at a general lemma

completely different method fro deriving the exhaust lemma

merged

merged

added example from the F-ing paper by Rossberg, Russo and Dreyer