# HG changeset patch
# User huffman
# Date 1338544438 -7200
# Node ID f02b4302d5dde3115dba3743b569cc21d814456e
# Parent  60bcc6cf17d6cacc73f3662b2c3e9879c680a0a5
remove duplicate lemma card_unit in favor of Finite_Set.card_UNIV_unit

diff -r 60bcc6cf17d6 -r f02b4302d5dd src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Jun 01 08:32:26 2012 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Jun 01 11:53:58 2012 +0200
@@ -2081,7 +2081,7 @@
   ultimately show "finite (UNIV :: 'b set)" by simp
 qed
 
-lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
+lemma card_UNIV_unit [simp]: "card (UNIV :: unit set) = 1"
   unfolding UNIV_unit by simp
 
 lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2"
diff -r 60bcc6cf17d6 -r f02b4302d5dd src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Fri Jun 01 08:32:26 2012 +0200
+++ b/src/HOL/Library/Cardinality.thy	Fri Jun 01 11:53:58 2012 +0200
@@ -41,9 +41,6 @@
   in [(@{const_syntax card}, card_univ_tr')] end
 *}
 
-lemma card_unit [simp]: "CARD(unit) = 1"
-  unfolding UNIV_unit by simp
-
 lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a::finite) * CARD('b::finite)"
   unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product)
 
diff -r 60bcc6cf17d6 -r f02b4302d5dd src/HOL/Library/Numeral_Type.thy
--- 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]