diff -r f4477d3fe520 -r 26c0c35641cb Nominal/Ex/ExCoreHaskell.thy
--- a/Nominal/Ex/ExCoreHaskell.thy	Sun Apr 18 09:26:38 2010 +0200
+++ b/Nominal/Ex/ExCoreHaskell.thy	Sun Apr 18 10:58:29 2010 +0200
@@ -679,5 +679,18 @@
   ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)
 qed
 
+section {* test about equivariance for alpha *}
+
+thm eqvts
+thm eqvts_raw
+
+declare permute_tkind_raw_permute_ckind_raw_permute_ty_raw_permute_ty_lst_raw_permute_co_raw_permute_co_lst_raw_permute_trm_raw_permute_assoc_lst_raw_permute_pat_raw_permute_vars_raw_permute_tvars_raw_permute_cvars_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_tkind_raw
+
+thm eqvts
+thm eqvts_raw
+
 end