| changeset 47210 | b1dd32b2a505 |
| parent 47209 | 4893907fe872 |
| child 47216 | 4d0878d54ca5 |
--- 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*}