added fundef_cong rule

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