--- a/Nominal/FSet.thy	Mon Apr 19 13:58:10 2010 +0200
+++ b/Nominal/FSet.thy	Mon Apr 19 14:08:01 2010 +0200
@@ -531,7 +531,7 @@
   by (lifting fcard_raw_suc_memb)
 
 lemma fin_fcard_not_0: "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"
-  by (lifting mem_card_not_0)
+  by (lifting memb_card_not_0)
 
 text {* funion *}
 
@@ -540,6 +540,10 @@
   and   "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
   by (lifting append.simps)
 
+lemma funion_empty[simp]:
+  shows "S |\<union>| {||} = S"
+  by (lifting append_Nil2)
+
 lemma funion_sym:
   shows "S |\<union>| T = T |\<union>| S"
   by (lifting funion_sym_pre)
@@ -548,6 +552,14 @@
   shows "S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)"
   by (lifting append_assoc)
 
+lemma singleton_union_left:
+  "{|a|} |\<union>| S = finsert a S"
+  by simp
+
+lemma singleton_union_right:
+  "S |\<union>| {|a|} = finsert a S"
+  by (subst funion_sym) simp
+
 section {* Induction and Cases rules for finite sets *}
 
 lemma fset_strong_cases: