src/HOL/Library/Cardinality.thy
changeset 48063 f02b4302d5dd
parent 48053 9bc78a08ff0a
child 48067 9f458b3efb5c
     1.1 --- a/src/HOL/Library/Cardinality.thy	Fri Jun 01 08:32:26 2012 +0200
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Fri Jun 01 11:53:58 2012 +0200
     1.3 @@ -41,9 +41,6 @@
     1.4    in [(@{const_syntax card}, card_univ_tr')] end
     1.5  *}
     1.6  
     1.7 -lemma card_unit [simp]: "CARD(unit) = 1"
     1.8 -  unfolding UNIV_unit by simp
     1.9 -
    1.10  lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a::finite) * CARD('b::finite)"
    1.11    unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product)
    1.12