Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Finite_Set.thy
changeset 45166 861ab6f9eb2b
parent 44928 7ef6505bde7f
child 45962 fc77947a7db4 
--- 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]:
isabelle