--- a/Nominal/Ex/Classical.thy	Tue Jul 19 01:40:36 2011 +0100
+++ b/Nominal/Ex/Classical.thy	Tue Jul 19 02:30:05 2011 +0100
@@ -382,17 +382,8 @@
 termination (eqvt)
   by lexicographic_order
 
-lemma crename_name_eqvt[eqvt]:
-  shows "p \<bullet> (M[d\<turnstile>c>e]) = (p \<bullet> M)[(p \<bullet> d)\<turnstile>c>(p \<bullet> e)]"
-apply(nominal_induct M avoiding: d e rule: trm.strong_induct)
-apply(auto)
-done
+thm crename.eqvt nrename.eqvt
 
-lemma nrename_name_eqvt[eqvt]:
-  shows "p \<bullet> (M[x\<turnstile>n>y]) = (p \<bullet> M)[(p \<bullet> x)\<turnstile>n>(p \<bullet> y)]"
-apply(nominal_induct M avoiding: x y rule: trm.strong_induct)
-apply(auto)
-done
 
 nominal_primrec 
   substn :: "trm \<Rightarrow> name   \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=<_>._}" [100,100,100,100] 100)