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