Nominal/nominal_dt_alpha.ML
2012-02-28 Cezary Kaliszyk Update to the localized quotient package
2012-02-17 Cezary Kaliszyk Update from Isabelle Wed Feb 15 23:19:30
2011-11-03 Christian Urban updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package
2011-09-21 Christian Urban deleted PNil
2011-07-07 Christian Urban code refactoring; introduced a record for raw_dt_info
2011-06-30 Christian Urban more code refactoring
2011-06-29 Christian Urban combined distributed data for alpha in alpha_result (partially done)
2011-06-29 Christian Urban moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
2011-06-28 Christian Urban some experiments
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-06-16 Christian Urban got rid of the boolean flag in the raw_equivariance function
2011-04-13 Christian Urban introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive
2010-12-16 Christian Urban simple cases for strong inducts done; infrastructure for the difficult ones is there
2010-12-06 Christian Urban automated alpha_perm_bn theorems
2010-12-06 Christian Urban ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
2010-12-03 Christian Urban updated to Isabelle 2nd December
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
2010-08-15 Christian Urban simplified code
2010-08-14 Christian Urban more experiments with lifting
2010-08-11 Christian Urban rsp for constructors
2010-08-11 Christian Urban added a function that transforms the helper-rsp lemmas into real rsp lemmas
2010-08-08 Christian Urban proved rsp-helper lemmas of size functions
2010-07-31 Christian Urban tuning
2010-07-31 Christian Urban further simplification with alpha_prove
2010-07-31 Christian Urban introduced a general alpha_prove method
2010-07-29 Christian Urban helper lemmas for rsp-lemmas
2010-07-27 Christian Urban cleaned up a bit Abs.thy
2010-07-19 Christian Urban minor polishing
2010-06-22 Christian Urban proved eqvip theorems for alphas
2010-06-22 Christian Urban prove that alpha implies alpha_bn (needed for rsp proofs)
2010-06-11 Christian Urban also symmetry
2010-06-10 Christian Urban premerge
2010-06-09 Christian Urban transitivity proofs done
2010-06-07 Christian Urban work on transitivity proof
2010-05-26 Christian Urban added FSet to the correct paper
2010-05-24 Christian Urban added slides
2010-05-24 Christian Urban tuned
2010-05-24 Christian Urban tuned
less more (0) tip