1.1 --- a/src/HOL/Finite_Set.thy	Fri Mar 30 09:08:29 2012 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Mar 30 08:04:28 2012 +0200
     1.3 @@ -2084,6 +2084,9 @@
     1.4  lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
     1.5    unfolding UNIV_unit by simp
     1.6  
     1.7 +lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2"
     1.8 +  unfolding UNIV_bool by simp
     1.9 +
    1.10  
    1.11  subsubsection {* Cardinality of image *}
    1.12  

     2.1 --- a/src/HOL/Nat_Numeral.thy	Fri Mar 30 09:08:29 2012 +0200
     2.2 +++ b/src/HOL/Nat_Numeral.thy	Fri Mar 30 08:04:28 2012 +0200
     2.3 @@ -132,9 +132,6 @@
     2.4  
     2.5  subsubsection{*Various Other Lemmas*}
     2.6  
     2.7 -lemma card_UNIV_bool[simp]: "card (UNIV :: bool set) = 2"
     2.8 -by(simp add: UNIV_bool)
     2.9 -
    2.10  text {*Evens and Odds, for Mutilated Chess Board*}
    2.11  
    2.12  text{*Lemmas for specialist use, NOT as default simprules*}