Nominal/nominal_function.ML
2011-07-18 Christian Urban added a flag (eqvt) to termination proofs arising fron nominal_primrecs
2011-06-16 Christian Urban added eqvt_at and invariant for boths sides of the equations
2011-06-16 Christian Urban added a test that every function must be of pt-sort
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
less more (0) -4 tip