src/HOL/Nat_Numeral.thy
changeset 31080 21ffc770ebc0
parent 31068 f591144b0f17
child 31096 e546e15089ef
child 31100 6a2e67fe4488
     1.1 --- a/src/HOL/Nat_Numeral.thy	Fri May 08 19:20:00 2009 +0200
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Sat May 09 07:25:22 2009 +0200
     1.3 @@ -982,6 +982,9 @@
     1.4  
     1.5  subsubsection{*Various Other Lemmas*}
     1.6  
     1.7 +lemma card_UNIV_bool[simp]: "card (UNIV :: bool set) = 2"
     1.8 +by(simp add: UNIV_bool)
     1.9 +
    1.10  text {*Evens and Odds, for Mutilated Chess Board*}
    1.11  
    1.12  text{*Lemmas for specialist use, NOT as default simprules*}