new simp lemma

--- a/src/HOL/Groups.thy	Sun Oct 28 11:00:09 2018 +0100
+++ b/src/HOL/Groups.thy	Sun Oct 28 14:08:05 2018 +0100
@@ -279,6 +279,9 @@
 sublocale add: comm_monoid plus 0
   by standard (simp add: ac_simps)
 
+lemma add_0_eq_id[simp]: "(+) 0 = (\<lambda>x. x)"
+by (auto simp: fun_eq_iff)
+
 end
 
 class monoid_mult = one + semigroup_mult +