Nominal/nominal_dt_rawfuns.ML
2011-04-13 Christian Urban introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive
2010-12-28 Christian Urban automated all strong induction lemmas
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-16 Christian Urban simple cases for strong inducts done; infrastructure for the difficult ones is there
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-08 Christian Urban moved definition of raw bn-functions into nominal_dt_rawfuns
2010-12-07 Christian Urban automated permute_bn theorems
2010-11-15 Christian Urban proved that bn functions return a finite set
2010-11-15 Christian Urban fixed bug in fv function where a shallow binder binds lists of names
2010-11-12 Christian Urban automated permute_bn functions (raw ones first)
2010-10-17 Christian Urban all tests work again
2010-10-14 Christian Urban major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
2010-09-10 Christian Urban tuned (to conform with indentation policy of Markus)
2010-09-03 Christian Urban made the fv-definition aggree more with alpha (needed in the support proofs)
less more (0) -15 tip