Nominal/Ex/LamTest.thy
2014-05-19 Christian Urban changed nominal_primrec into the more appropriate nominal_function
2012-01-03 Christian Urban updated to explicit set type constructor (post Isabelle 3rd January)
2011-01-17 Christian Urban eliminated tracing code; added flag so that equivariance is only proved for the function graph, not the relation
2011-01-15 Christian Urban subst also works now
2011-01-15 Christian Urban nominal_function works now completely for frees and depth; still a propbelm with subst; no unproved assumptions
2011-01-10 Christian Urban a few lemmas about freshness for at and at_base
2011-01-10 Christian Urban added a property about finite support in the presense of eqvt_at
less more (0) -10 -7 tip