| 2011-07-18 | Christian Urban | added a flag (eqvt) to termination proofs arising fron nominal_primrecs | file | diff | annotate |
| 2011-06-16 | Christian Urban | added eqvt_at and invariant for boths sides of the equations | file | diff | annotate |
| 2011-06-16 | Christian Urban | added a test that every function must be of pt-sort | file | diff | annotate |
| 2011-06-07 | Christian Urban | fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant | file | diff | annotate |