# HG changeset patch
# User nipkow
# Date 1466895783 -7200
# Node ID bf2cf06537411435fc18e7c0fdb7d363b8fab2c8
# Parent  77332fed33c3019acf2400f1372af4c1e9ef448b
added fundef_cong rule

diff -r 77332fed33c3 -r bf2cf0653741 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Fri Jun 24 20:27:57 2016 +0200
+++ b/src/HOL/Groups_Big.thy	Sun Jun 26 01:03:03 2016 +0200
@@ -133,7 +133,7 @@
   with False show ?thesis by simp
 qed
 
-lemma cong:
+lemma cong [fundef_cong]:
   assumes "A = B"
   assumes g_h: "\<And>x. x \<in> B \<Longrightarrow> g x = h x"
   shows "F g A = F h B"