# HG changeset patch
# User bulwahn
# Date 1318944438 -7200
# Node ID 861ab6f9eb2b4352873f291e6faa5b3e60e3dc3a
# Parent  f4896c792316a756e353a102d7e8772d681cae14
tuned

diff -r f4896c792316 -r 861ab6f9eb2b src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Oct 18 15:27:17 2011 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Oct 18 15:27:18 2011 +0200
@@ -1859,7 +1859,7 @@
 by (simp add: card_Suc_Diff1 [symmetric])
 
 lemma card_Diff_singleton_if:
-  "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
+  "finite A ==> card (A - {x}) = (if x : A then card A - 1 else card A)"
 by (simp add: card_Diff_singleton)
 
 lemma card_Diff_insert[simp]: