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