| changeset 19870 | ef037d1b32d1 |
| parent 19868 | e93ffc043dfd |
| child 19931 | fb32b43e7f80 |
--- 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 *}