src/HOL/Groups.thy
changeset 44348 40101794c52f
parent 42248 04bffad68aa4
child 44433 9fbee4aab115
     1.1 --- a/src/HOL/Groups.thy	Sat Aug 20 12:51:15 2011 -0700
     1.2 +++ b/src/HOL/Groups.thy	Sat Aug 20 13:07:00 2011 -0700
     1.3 @@ -411,6 +411,10 @@
     1.4    ultimately show "a = - b" by simp
     1.5  qed
     1.6  
     1.7 +lemma add_eq_0_iff: "x + y = 0 \<longleftrightarrow> y = - x"
     1.8 +  unfolding eq_neg_iff_add_eq_0 [symmetric]
     1.9 +  by (rule equation_minus_iff)
    1.10 +
    1.11  end
    1.12  
    1.13  class ab_group_add = minus + uminus + comm_monoid_add +
    1.14 @@ -466,7 +470,7 @@
    1.15  (* FIXME: duplicates right_minus_eq from class group_add *)
    1.16  (* but only this one is declared as a simp rule. *)
    1.17  lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
    1.18 -by (simp add: algebra_simps)
    1.19 +  by (rule right_minus_eq)
    1.20  
    1.21  lemma diff_eq_diff_eq:
    1.22    "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"