author | krauss |
Thu, 15 Feb 2007 12:14:34 +0100 | |
changeset 22324 | c95319d14332 |
parent 22323 | b8c227d8ca91 |
child 22325 | be61bd159a99 |
--- 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