src/HOL/Datatype.thy
changeset 24286 7619080e49f0
parent 24194 96013f81faef
child 24699 c6674504103f
     1.1 --- a/src/HOL/Datatype.thy	Wed Aug 15 09:02:11 2007 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Wed Aug 15 12:52:56 2007 +0200
     1.3 @@ -556,6 +556,8 @@
     1.4    inject Pair_eq
     1.5    induction prod_induct
     1.6  
     1.7 +declare prod.size [noatp]
     1.8 +
     1.9  lemmas prod_caseI = prod.cases [THEN iffD2, standard]
    1.10  
    1.11  lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"