Nominal/Ex/Lambda.thy
2012-06-04 Christian Urban added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often
2012-05-31 Christian Urban added to the simplifier nominal_datatype.fresh lemmas
2012-05-23 Christian Urban improved handling in the simplifier for inequalities derived from freshness assumptions
2012-04-10 Christian Urban updated to latest changes (10 April) to quotient package (lift_raw_const only takes dummy theorem TrueI....in the future this will not work anymore)
2012-03-17 Christian Urban updated to new Isabelle (declared keywords)
2011-12-21 Cezary Kaliszyk Port CR_Takahashi from Nominal1, no more "sorry" in BetaCR.
2011-12-17 Christian Urban cleaned examples for stable branch Nominal2-Isabelle2011-1
2011-12-15 Christian Urban updated to lates changes in the datatype package
2011-11-08 Cezary Kaliszyk Add equivariance for alpha_lam_raw and abs_lam.
2011-11-07 Christian Urban all examples work again after quotient package has been "de-localised"
2011-08-19 Cezary Kaliszyk Comment out examples with 'True' that do not work because function still does not work
2011-07-22 Christian Urban completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list
2011-07-19 Christian Urban preliminary version of automatically generation the eqvt-lemmas for functions defined with nominal_primrec
2011-07-19 Christian Urban generated the partial eqvt-theorem for functions
less more (0) -100 -14 tip