src/HOL/Algebra/Ring.thy
changeset 68399 0b71d08528f0
parent 67613 ce654b0e6d69
child 68443 43055b016688
     1.1 --- a/src/HOL/Algebra/Ring.thy	Tue Jun 05 16:35:52 2018 +0200
     1.2 +++ b/src/HOL/Algebra/Ring.thy	Wed Jun 06 14:25:53 2018 +0100
     1.3 @@ -184,8 +184,6 @@
     1.4    "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y \<in> carrier G"
     1.5    by (simp add: a_minus_def)
     1.6  
     1.7 -lemmas a_l_cancel = add.l_cancel
     1.8 -lemmas a_r_cancel = add.r_cancel
     1.9  lemmas l_neg = add.l_inv [simp del]
    1.10  lemmas r_neg = add.r_inv [simp del]
    1.11  lemmas minus_zero = add.inv_one