Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authorbulwahn
Tue, 18 Oct 2011 15:27:18 +0200
changeset 45166 861ab6f9eb2b
parent 45165 f4896c792316
child 45167 6bc8d260d459
tuned
src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions 
--- 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