src/HOL/FunDef.thy

--- a/src/HOL/FunDef.thy	Wed Jun 21 10:26:39 2006 +0200
+++ b/src/HOL/FunDef.thy	Wed Jun 21 11:08:04 2006 +0200
@@ -86,4 +86,10 @@
   let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
 
 
+lemma split_cong[fundef_cong]:
+  "\<lbrakk> \<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y; p = q \<rbrakk> 
+  \<Longrightarrow> split f p = split g q"
+  by (auto simp:split_def)
+
+
 end