Quot/Nominal/nominal_permeq.ML
2010-02-03 Christian Urban added a first eqvt_tac which pushes permutations inside terms
less more (0) tip