src/HOL/Nominal/Nominal.thy

 (*******************************************************)
 (* Setup of the theorem attributes eqvt, fresh and bij *)
 use "nominal_thmdecls.ML"
 setup "NominalThmDecls.setup"
 
+lemmas  [eqvt] = perm_list.simps perm_prod.simps 
+
+
+
 (***************************************)
 (* setup for the individial atom-kinds *)
 (* and nominal datatypes               *)
 use "nominal_atoms.ML"
 (* permutation equality tactic *)