# HG changeset patch
# User krauss
# Date 1150880884 -7200
# Node ID 8190655ea2d4a617e59447ed2cfefa65b299c29a
# Parent  16a5037f2d25cdb5fecdc0826feda98be078f8bc
Added split_cong rule

diff -r 16a5037f2d25 -r 8190655ea2d4 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