equal
deleted
inserted
replaced
635 by (simp only: internal_split_def split_conv) |
635 by (simp only: internal_split_def split_conv) |
636 |
636 |
637 use "Tools/split_rule.ML" |
637 use "Tools/split_rule.ML" |
638 setup Split_Rule.setup |
638 setup Split_Rule.setup |
639 |
639 |
640 hide const internal_split |
640 hide_const internal_split |
641 |
641 |
642 |
642 |
643 lemmas prod_caseI = prod.cases [THEN iffD2, standard] |
643 lemmas prod_caseI = prod.cases [THEN iffD2, standard] |
644 |
644 |
645 lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p" |
645 lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p" |