--- a/Nominal/Ex/SingleLet.thy	Sat Sep 04 06:10:04 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sat Sep 04 06:23:31 2010 +0800
@@ -34,12 +34,6 @@
 thm single_let.supports
 thm single_let.fsupp
 
-lemma Abs_eq_iff:
-  shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
-  and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
-  and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
-  by (lifting alphas_abs)
-
 lemma test2:
   assumes "fv_trm t = supp t" 
   shows "\<forall>p. fv_trm (p \<bullet> t) = supp (p \<bullet> t)"