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/Library/Cardinality.thy
changeset 53191 14ab2f821e1d
parent 53015 a1119cf551e8
child 53745 788730ab7da4 
--- a/src/HOL/Library/Cardinality.thy	Sun Aug 25 17:04:22 2013 +0200
+++ b/src/HOL/Library/Cardinality.thy	Sun Aug 25 17:17:48 2013 +0200
@@ -64,7 +64,7 @@
 proof -
   have "(None :: 'a option) \<notin> range Some" by clarsimp
   thus ?thesis
-    by(simp add: UNIV_option_conv card_eq_0_iff finite_range_Some card_insert_disjoint card_image)
+    by (simp add: UNIV_option_conv card_eq_0_iff finite_range_Some card_image)
 qed
 
 lemma card_option [simp]: "CARD('a option) = Suc CARD('a::finite)"
isabelle