--- a/Nominal/Ex/Classical.thy	Fri Apr 16 11:09:32 2010 +0200
+++ b/Nominal/Ex/Classical.thy	Fri Apr 16 16:29:11 2010 +0200
@@ -63,6 +63,14 @@
    alpha (ImpR_raw coname1 name trm_raw coname2)
          (ImpR_raw coname1a namea trm_rawa coname2a)"
 
+thm alpha.intros
+
+declare permute_trm_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha
+thm eqvts_raw
+
 
 end