equal
deleted
inserted
replaced
553 induction unit_induct |
553 induction unit_induct |
554 |
554 |
555 rep_datatype prod |
555 rep_datatype prod |
556 inject Pair_eq |
556 inject Pair_eq |
557 induction prod_induct |
557 induction prod_induct |
|
558 |
|
559 declare prod.size [noatp] |
558 |
560 |
559 lemmas prod_caseI = prod.cases [THEN iffD2, standard] |
561 lemmas prod_caseI = prod.cases [THEN iffD2, standard] |
560 |
562 |
561 lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p" |
563 lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p" |
562 by auto |
564 by auto |