new simp lemma draft
authornipkow
Sun, 28 Oct 2018 14:08:05 +0100
changeset 69204 8476cf7b4d8c
parent 69203 0b61266fc2e0
new simp lemma
src/HOL/Groups.thy
--- 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 +