src/HOL/Product_Type.thy
changeset 35365 2fcd08c62495
parent 35364 b8c62d60195c
child 35427 ad039d29e01c
equal deleted inserted replaced
35364:b8c62d60195c 35365:2fcd08c62495
   633 
   633 
   634 lemma internal_split_conv: "internal_split c (a, b) = c a b"
   634 lemma internal_split_conv: "internal_split c (a, b) = c a b"
   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 SplitRule.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]