diff -r 632b08744613 -r 3cf30bb8c6f6 Nominal/Term5.thy
--- a/Nominal/Term5.thy	Thu Mar 11 13:34:45 2010 +0100
+++ b/Nominal/Term5.thy	Thu Mar 11 13:44:54 2010 +0100
@@ -48,20 +48,10 @@
   done
 
 lemma alpha5_eqvt:
-  "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"
-  "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"
-  "alpha_rbv5 a b c \<Longrightarrow> alpha_rbv5 (x \<bullet> a) (x \<bullet> b) (x \<bullet> c)"
-apply (induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)
-apply (simp_all add: alpha5_inj permute_eqvt[symmetric])
-apply (erule exE)
-apply (rule_tac x="x \<bullet> pi" in exI)
-apply (erule conjE)+
-apply (rule conjI)
-apply (erule alpha_gen_compose_eqvt)
-apply (simp_all add: eqvts)
-apply (simp add: permute_eqvt[symmetric])
-apply (subst eqvts[symmetric])
-apply (simp add: eqvts)
+  "(xa \<approx>5 y \<longrightarrow> (p \<bullet> xa) \<approx>5 (p \<bullet> y)) \<and>
+  (xb \<approx>l ya \<longrightarrow> (p \<bullet> xb) \<approx>l (p \<bullet> ya)) \<and>
+  (alpha_rbv5 a b c \<longrightarrow> alpha_rbv5 (p \<bullet> a) (p \<bullet> b) (p \<bullet> c))"
+apply (tactic {* alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} @{context} 1 *})
 done
 
 lemma alpha5_equivp: