# HG changeset patch
# User paulson
# Date 1112699120 -7200
# Node ID 157f3988f7752bf325e6bc67b202f28aa3dcb5ef
# Parent  d53e5370cfbfc3bc5c541afafeb8554c576ca167
arg_cong2 by Norbert Voelker

diff -r d53e5370cfbf -r 157f3988f775 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Apr 05 08:03:52 2005 +0200
+++ b/src/HOL/HOL.thy	Tue Apr 05 13:05:20 2005 +0200
@@ -270,6 +270,12 @@
 apply (rule refl)
 done
 
+lemma arg_cong2: "\<lbrakk> a = b; c = d \<rbrakk> \<Longrightarrow> f a c = f b d"
+apply (erule ssubst)+
+apply (rule refl)
+done
+
+
 lemma cong: "[| f = g; (x::'a) = y |] ==> f(x) = g(y)"
 apply (erule subst)+
 apply (rule refl)