diff -r 3b8741ecfda3 -r 8054f4988672 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Fri Oct 15 16:23:26 2010 +0900
+++ b/Nominal/FSet.thy	Fri Oct 15 16:32:34 2010 +0900
@@ -824,10 +824,8 @@
   by (descending) (auto simp add: fcard_raw_def card_gt_0_iff)
   
 lemma fcard_not_fin:
-  assumes a: "x |\<notin>| S" 
-  shows "fcard (finsert x S) = Suc (fcard S)"
-  using a
-  by (descending) (simp add: memb_def fcard_raw_def)
+  shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
+  by (descending) (auto simp add: memb_def fcard_raw_def insert_absorb)
 
 lemma fcard_suc: 
   shows "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n"
@@ -1204,7 +1202,7 @@
   by (rule card_Diff2_less[OF finite_fset])
 
 lemma fcard_delete1_le: 
-  shows "fcard (fdelete x xs) <= fcard xs"
+  shows "fcard (fdelete x xs) \<le> fcard xs"
   unfolding fdelete_set fcard_set
   by (rule card_Diff1_le[OF finite_fset])