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