| 2012-08-07 | Christian Urban | definition of an auxiliary graph in nominal-primrec definitions | file | diff | annotate |
| 2012-07-15 | Christian Urban | added a simproc for alpha-equivalence to the simplifier | file | diff | annotate |
| 2012-06-04 | Christian Urban | added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often | file | diff | annotate |
| 2011-07-19 | Christian Urban | preliminary version of automatically generation the eqvt-lemmas for functions defined with nominal_primrec | file | diff | annotate |
| 2011-07-19 | Christian Urban | generated the partial eqvt-theorem for functions | file | diff | annotate |
| 2011-07-18 | Christian Urban | added a flag (eqvt) to termination proofs arising fron nominal_primrecs | file | diff | annotate |
| 2011-07-17 | Christian Urban | some tuning | file | diff | annotate |