--- a/Quot/Nominal/LamEx.thy	Tue Feb 02 09:51:39 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Tue Feb 02 10:20:54 2010 +0100
@@ -2,52 +2,6 @@
 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs"
 begin
 
-
-(* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
-lemma in_permute_iff:
-  shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
-apply(unfold mem_def permute_fun_def)[1]
-apply(simp add: permute_bool_def) 
-done
-
-lemma fresh_star_permute_iff:
-  shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
-apply(simp add: fresh_star_def)
-apply(auto)
-apply(drule_tac x="p \<bullet> xa" in bspec)
-apply(unfold mem_def permute_fun_def)[1] 
-apply(simp add: eqvts)
-apply(simp add: fresh_permute_iff)
-apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1])
-apply(simp)
-apply(drule_tac x="- p \<bullet> xa" in bspec)
-apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1])
-apply(simp)
-apply(simp)
-done
-
-lemma fresh_minus_perm:
-  fixes p::perm
-  shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p"
-  apply(simp add: fresh_def)
-  apply(simp only: supp_minus_perm)
-  done
-
-lemma fresh_plus:
-  fixes p q::perm
-  shows "\<lbrakk>a \<sharp> p;  a \<sharp> q\<rbrakk> \<Longrightarrow> a \<sharp> (p + q)"
-unfolding fresh_def
-using supp_plus_perm
-apply(auto)
-done
-
-lemma fresh_star_plus:
-  fixes p q::perm
-  shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
-unfolding fresh_star_def
-by (simp add: fresh_plus)
-
-
 atom_decl name
 
 datatype rlam =