diff -r eba1b9e7c458 -r ef037d1b32d1 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Jun 13 15:07:47 2006 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Jun 13 15:07:58 2006 +0200
@@ -236,6 +236,9 @@
    apply (subst insert_Diff, simp_all)
   done
 
+lemma finite_Diff_singleton [simp]: "finite (A - {a}) = finite A"
+  by simp
+
 
 text {* Image and Inverse Image over Finite Sets *}