--- a/Nominal/Nominal2_FSet.thy	Wed May 26 15:37:56 2010 +0200
+++ b/Nominal/Nominal2_FSet.thy	Thu May 27 18:37:52 2010 +0200
@@ -1,8 +1,14 @@
 theory Nominal2_FSet
 imports "../Nominal-General/Nominal2_Supp"
+        "../Nominal-General/Nominal2_Atoms" 
+        "../Nominal-General/Nominal2_Eqvt" 
         FSet 
 begin
 
+lemma "p \<bullet> {} = {}"
+apply(perm_simp)
+by simp
+
 lemma permute_rsp_fset[quot_respect]:
   "(op = ===> list_eq ===> list_eq) permute permute"
   apply (simp add: eqvts[symmetric])
@@ -34,12 +40,29 @@
 
 end
 
-lemma permute_fset[simp, eqvt]:
+lemma "p \<bullet> {} = {}"
+apply(perm_simp)
+by simp
+
+lemma permute_fset[simp]:
   fixes S::"('a::pt) fset"
   shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
   and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)"
   by (lifting permute_list.simps)
 
+lemma "p \<bullet> {} = {}"
+apply(perm_simp)
+by simp
+
+ML {* @{term "{}"} ; @{term "{||}"} *}
+
+declare permute_fset[eqvt]
+
+lemma "p \<bullet> {} = {}"
+apply(perm_simp)
+by simp
+
+
 lemma fmap_eqvt[eqvt]: 
   shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)"
   by (lifting map_eqvt)
@@ -119,4 +142,8 @@
   apply auto
   done
 
+lemma "p \<bullet> {} = {}"
+apply(perm_simp)
+by simp
+
 end