diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/ExPS8.thy
--- a/Nominal/Ex/ExPS8.thy	Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Ex/ExPS8.thy	Mon May 10 15:45:04 2010 +0200
@@ -48,6 +48,11 @@
 thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv
 thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff
 
+
+declare permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_exp_raw
 end