2011-01-15 Christian Urban nominal_function works now completely for frees and depth; still a propbelm with subst; no unproved assumptions
2011-01-14 Christian Urban strengthened renaming lemmas
2011-01-13 Christian Urban added eqvt_lemmas for subset and psubset
2011-01-10 Christian Urban a few lemmas about freshness for at and at_base
2011-01-10 Christian Urban added a property about finite support in the presense of eqvt_at
2011-01-09 Christian Urban instantiated fundef_ex1_eqvt_at theorem with the indction hypothesis
2011-01-09 Christian Urban solved subgoals for depth and subst function
2011-01-09 Christian Urban added eqvt_at premises in function definition - however not proved at the moment
2011-01-07 Christian Urban added one further lemma about equivariance of THE_default
2011-01-07 Christian Urban equivariance of THE_default under the uniqueness assumption
2011-01-07 Christian Urban derived equivariance for the function graph and function relation
2011-01-06 Christian Urban a modified function package where, as a test, True has been injected into the compatibility condictions
2011-01-06 Christian Urban removed last traces of debugging code
2011-01-06 Christian Urban removed debugging code abd introduced a guarded tracing function
2011-01-06 Christian Urban moved Weakening up....it does not compile when put at the last position
2011-01-06 Christian Urban tuned
2011-01-06 Christian Urban added weakening to the test cases
2011-01-06 Christian Urban cleaned up weakening proof and added a version with finit sets
2011-01-06 Christian Urban same
2011-01-06 Christian Urban some further lemmas for fsets
2011-01-06 Christian Urban made sure the raw datatypes and raw functions do not get any mixfix syntax
2011-01-05 Christian Urban exported the code into a separate file
2011-01-05 Christian Urban strong rule inductions; as an example the weakening lemma works
2011-01-04 Christian Urban final version of the ESOP paper; used set+ instead of res as requested by one reviewer
2011-01-03 Christian Urban file with most of the strong rule induction development
2011-01-03 Christian Urban simple cases for string rule inductions
2010-12-31 Christian Urban changed res keyword to set+ for restrictions; comment by a referee
2010-12-31 Christian Urban added proper case names for all induct and exhaust theorems
2010-12-31 Christian Urban added small example for strong inductions; functions still need a sorry
2010-12-30 Christian Urban removed local fix for bug in induction_schema; added setup method for strong inductions
2010-12-28 Christian Urban automated all strong induction lemmas
2010-12-28 Christian Urban proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
2010-12-26 Christian Urban generated goals for strong induction theorems.
2010-12-23 Christian Urban test with strong inductions
2010-12-23 Christian Urban moved all strong_exhaust code to nominal_dt_quot; tuned examples
2010-12-23 Christian Urban moved generic functions into nominal_library
2010-12-22 Christian Urban slight tuning
2010-12-22 Christian Urban slight tuning
2010-12-22 Christian Urban tuned examples
2010-12-22 Christian Urban added fold_right which produces the correct term for left-infix operators
2010-12-22 Christian Urban updated to Isabelle 22 December
2010-12-22 Christian Urban a bit tuning
2010-12-22 Christian Urban corrected premises of strong exhausts theorems
2010-12-22 Christian Urban properly exported strong exhaust theorem; cleaned up some examples
2010-12-21 Christian Urban all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
2010-12-19 Christian Urban one interesting case done
2010-12-19 Christian Urban a stronger statement for at_set_avoiding
2010-12-17 Christian Urban tuned
2010-12-17 Christian Urban tuned
2010-12-16 Christian Urban simple cases for strong inducts done; infrastructure for the difficult ones is there
2010-12-16 Christian Urban added theorem-rewriter conversion
2010-12-14 Christian Urban freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through)
2010-12-12 Christian Urban created strong_exhausts terms
2010-12-12 Christian Urban moved setify and listify functions into the library; introduced versions that have a type argument
2010-12-10 Christian Urban updated
2010-12-09 Christian Urban a bit more tuning of the paper
2010-12-09 Christian Urban brought the paper to 20 pages plus one page appendix
2010-12-08 Christian Urban first tests about exhaust
2010-12-08 Christian Urban moved some code into the nominal_library
2010-12-08 Christian Urban moved definition of raw bn-functions into nominal_dt_rawfuns
(0) -1000 -300 -100 -60 +60 +100 +300 tip