src/HOL/Product_Type.thy

--- a/src/HOL/Product_Type.thy	Mon Nov 06 16:28:35 2006 +0100
+++ b/src/HOL/Product_Type.thy	Mon Nov 06 16:28:36 2006 +0100
@@ -759,6 +759,17 @@
 setup SplitRule.setup
 
 
+subsection {* Further lemmas *}
+
+lemma
+  split_Pair: "split Pair x = x"
+  unfolding split_def by auto
+
+lemma
+  split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
+  by (cases x, simp)
+
+
 subsection {* Code generator setup *}
 
 instance unit :: eq ..