Nominal/nominal_dt_rawfuns.ML
2011-06-23 Christian Urban fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package
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)
2010-08-26 Christian Urban corrected bug with fv-function generation (that was the problem with recursive binders)
2010-08-25 Christian Urban can now deal with type variables in nominal datatype definitions
2010-08-17 Christian Urban improved runtime slightly, by constructing an explicit size measure for the function definitions
2010-08-17 Christian Urban more tuning of the code
2010-08-17 Christian Urban improved code
2010-07-29 Christian Urban equivariance for size
2010-07-27 Christian Urban cleaned up a bit Abs.thy
2010-07-27 Christian Urban fixed order of fold_union to make alpha and fv agree
2010-07-19 Christian Urban minor polishing
2010-06-22 Christian Urban cleaned up the FSet (noise was introduced by error)
2010-06-07 Christian Urban work on transitivity proof
2010-06-03 Christian Urban fixed problem with eqvt proofs
2010-06-02 Christian Urban fixed problem with bn_info
2010-06-01 Christian Urban smaller code for raw-eqvt proofs
2010-05-31 Christian Urban all raw definitions are defined using function
2010-05-24 Christian Urban tuned
2010-05-24 Christian Urban alpha works now
2010-05-23 Christian Urban started to work on alpha
2010-05-22 Christian Urban properly exported bn_descr
2010-05-21 Christian Urban hving a working fv-definition without the export
2010-05-21 Christian Urban tuned
2010-05-20 Christian Urban tuned
2010-05-20 Christian Urban moved some mk_union and mk_diff into the library
2010-05-20 Christian Urban new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
less more (0) tip