--- a/Quot/Nominal/LamEx2.thy	Mon Feb 08 11:56:22 2010 +0100
+++ b/Quot/Nominal/LamEx2.thy	Mon Feb 08 13:12:55 2010 +0100
@@ -2,22 +2,6 @@
 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs" "../QuotProd"
 begin
 
-
-(* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
-(* Currently not used, still needed needed? *)
-lemma supp_finite_set:
-  fixes S::"atom set"
-  assumes "finite S"
-  shows "supp S = S"
-  apply(rule finite_supp_unique)
-  apply(simp add: supports_def)
-  apply(auto simp add: permute_set_eq swap_atom)[1]
-  apply(metis)
-  apply(rule assms)
-  apply(auto simp add: permute_set_eq swap_atom)[1]
-done
-  
-
 atom_decl name
 
 datatype rlam =
@@ -324,7 +308,6 @@
 apply auto
 done
 
-(*
 (* pi_abs would be also sufficient to prove the next lemma *)
 lemma replam_eqvt: "pi \<bullet> (rep_lam x) = rep_lam (pi \<bullet> x)"
 apply (unfold rep_lam_def)
@@ -338,7 +321,7 @@
 apply (simp only: Quotient_abs_rep[OF Quotient_lam])
 apply auto
 done
-*)
+
 
 lemma alpha_prs [quot_preserve]: "(rep_lam ---> rep_lam ---> id) alpha = (op =)"
 apply (simp add: expand_fun_eq)