--- a/Nominal/Ex/ExLF.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/ExLF.thy	Sun May 09 12:26:10 2010 +0100
@@ -20,6 +20,14 @@
 
 thm kind_ty_trm.supp
 
+declare permute_kind_raw_permute_ty_raw_permute_trm_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
+
+
+
 end