# HG changeset patch # User Cezary Kaliszyk # 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 \ (bi b)) = bi (p \ 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