| changeset 47210 | b1dd32b2a505 |
| parent 46898 | 1570b30ee040 |
| child 47221 | 7205eb4a0a05 |
--- 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 *}