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/Numeral_Type.thy
changeset 48063 f02b4302d5dd
parent 47108 2a1953f0d20d
child 49834 b27bbb021df1 
--- a/src/HOL/Library/Numeral_Type.thy	Fri Jun 01 08:32:26 2012 +0200
+++ b/src/HOL/Library/Numeral_Type.thy	Fri Jun 01 11:53:58 2012 +0200
@@ -31,7 +31,7 @@
 
 lemma card_num1 [simp]: "CARD(num1) = 1"
   unfolding type_definition.card [OF type_definition_num1]
-  by (simp only: card_unit)
+  by (simp only: card_UNIV_unit)
 
 lemma card_bit0 [simp]: "CARD('a bit0) = 2 * CARD('a::finite)"
   unfolding type_definition.card [OF type_definition_bit0]
isabelle