# HG changeset patch
# User krauss
# Date 1171538074 -3600
# Node ID c95319d143322b39c1011eb64f45677bc5edb442
# Parent  b8c227d8ca913b20247c87c4242173b7d4047a62
added congruence rule for function composition

diff -r b8c227d8ca91 -r c95319d14332 src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Thu Feb 15 12:02:11 2007 +0100
+++ b/src/HOL/FunDef.thy	Thu Feb 15 12:14:34 2007 +0100
@@ -126,5 +126,9 @@
   \<Longrightarrow> split f p = split g q"
   by (auto simp:split_def)
 
+lemma comp_cong[fundef_cong]:
+  "f (g x) = f' (g' x')
+  ==>  (f o g) x = (f' o g') x'"
+unfolding o_apply .
 
 end