drop redundant sort constraint
authorAndreas Lochbihler
Fri Jun 01 13:52:51 2012 +0200 (2012-06-01)
changeset 4805811a732f7d79f
parent 48054 60bcc6cf17d6
child 48059 f6ce99d3719b
drop redundant sort constraint
src/HOL/Library/Cardinality.thy
     1.1 --- a/src/HOL/Library/Cardinality.thy	Fri Jun 01 08:32:26 2012 +0200
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Fri Jun 01 13:52:51 2012 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4  lemma card_unit [simp]: "CARD(unit) = 1"
     1.5    unfolding UNIV_unit by simp
     1.6  
     1.7 -lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a::finite) * CARD('b::finite)"
     1.8 +lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a) * CARD('b)"
     1.9    unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product)
    1.10  
    1.11  lemma card_sum [simp]: "CARD('a + 'b) = CARD('a::finite) + CARD('b::finite)"