# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268641645 -3600
# Node ID 14b850159df13d1dc83f84c6ff86e95518ed554a
# Parent  ffd5540ac2e97bbae59bc3b49cba5c0a3488cc4d
Use eqvt.

diff -r ffd5540ac2e9 -r 14b850159df1 Nominal/Test.thy
--- a/Nominal/Test.thy	Mon Mar 15 08:39:23 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 15 09:27:25 2010 +0100
@@ -35,13 +35,7 @@
 
 lemma bi_eqvt:
   shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"
-apply(induct b rule: lam_bp_inducts(2))
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp add: lam_bp_bn lam_bp_perm)
-apply(simp add: eqvts)
-done
+  by (rule eqvts)
 
 lemma supp_fv:
   "supp t = fv_lam t" and