arg_cong2 by Norbert Voelker

--- 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)