Nominal/nominal_dt_alpha.ML
2010-11-13 Christian Urban respectfulness for permute_bn functions
2010-11-12 Christian Urban automated permute_bn functions (raw ones first)
2010-11-10 Christian Urban adapted to changes by Florian on the quotient package and removed local fix for function package
2010-09-20 Christian Urban introduced a general procedure for structural inductions; simplified reflexivity proof
2010-09-12 Christian Urban tuned code
2010-09-10 Christian Urban tuned (to conform with indentation policy of Markus)
2010-09-10 Christian Urban supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
2010-09-03 Christian Urban renamed alpha_gen -> alpha_set and Abs -> Abs_set etc
2010-09-03 Christian Urban made the fv-definition aggree more with alpha (needed in the support proofs)
2010-08-26 Christian Urban "isabelle make test" makes all major examples....they work up to supp theorems (excluding)
2010-08-26 Christian Urban corrected bug with fv-function generation (that was the problem with recursive binders)
2010-08-25 Christian Urban cleaning of unused files and code
2010-08-25 Christian Urban can now deal with type variables in nominal datatype definitions
2010-08-17 Christian Urban improved code
2010-08-16 Christian Urban added rsp-lemmas for alpha_bns
less more (0) -15 tip