--- a/src/HOL/Finite_Set.thy Fri Mar 30 09:08:29 2012 +0200
+++ b/src/HOL/Finite_Set.thy Fri Mar 30 08:04:28 2012 +0200
@@ -2084,6 +2084,9 @@
lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
unfolding UNIV_unit by simp
+lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2"
+ unfolding UNIV_bool by simp
+
subsubsection {* Cardinality of image *}
--- a/src/HOL/Nat_Numeral.thy Fri Mar 30 09:08:29 2012 +0200
+++ b/src/HOL/Nat_Numeral.thy Fri Mar 30 08:04:28 2012 +0200
@@ -132,9 +132,6 @@
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*}