diff -r abd46dfc0212 -r f38adea0591c Nominal-General/Nominal2_Eqvt.thy --- a/Nominal-General/Nominal2_Eqvt.thy Thu May 13 17:41:28 2010 +0100 +++ b/Nominal-General/Nominal2_Eqvt.thy Thu May 13 18:19:48 2010 +0100 @@ -302,7 +302,7 @@ imp_eqvt [folded induct_implies_def] (* nominal *) - supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt + supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt (* datatypes *) Pair_eqvt permute_list.simps