Nominal/Ex/LetRec.thy
2014-05-19 Christian Urban changed nominal_primrec into the more appropriate nominal_function
2012-08-07 Christian Urban definition of an auxiliary graph in nominal-primrec definitions
2012-07-15 Christian Urban added a simproc for alpha-equivalence to the simplifier
2012-06-04 Christian Urban added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often
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
2011-07-18 Christian Urban added a flag (eqvt) to termination proofs arising fron nominal_primrecs
2011-07-17 Christian Urban some tuning
2011-07-05 Christian Urban changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
2011-06-20 Cezary Kaliszyk function for let-rec
2010-08-29 Christian Urban renamed NewParser to Nominal2
2010-08-26 Christian Urban corrected bug with fv-function generation (that was the problem with recursive binders)
2010-08-25 Christian Urban cleaned up (almost completely) the examples
less more (0) tip