# HG changeset patch
# User huffman
# Date 1333087468 -7200
# Node ID b1dd32b2a505fdf77fd15a4b0c51e18a5230f5d8
# Parent  4893907fe872a076bc32581e40a89a54f411e802
move lemma card_UNIV_bool from Nat_Numeral.thy to Finite_Set.thy

diff -r 4893907fe872 -r b1dd32b2a505 src/HOL/Finite_Set.thy
--- 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 *}
 
diff -r 4893907fe872 -r b1dd32b2a505 src/HOL/Nat_Numeral.thy
--- 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*}