src/HOL/Product_Type.thy
changeset 26143 314c0bcb7df7
parent 25885 6fbc3f54f819
child 26340 a85fe32e7b2f
     1.1 --- a/src/HOL/Product_Type.thy	Tue Feb 26 07:59:59 2008 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Feb 26 11:18:43 2008 +0100
     1.3 @@ -821,6 +821,10 @@
     1.4    "prod_case = split"
     1.5    by (auto simp add: expand_fun_eq)
     1.6  
     1.7 +lemma prod_case_beta:
     1.8 +  "prod_case f p = f (fst p) (snd p)"
     1.9 +  unfolding prod_case_split split_beta ..
    1.10 +
    1.11  
    1.12  subsection {* Further cases/induct rules for tuples *}
    1.13