src/HOL/Rings.thy
changeset 61649 268d88ec9087
parent 60867 86e7560e07d0
child 61762 d50b993b4fb9
     1.1 --- a/src/HOL/Rings.thy	Thu Nov 12 11:22:26 2015 +0100
     1.2 +++ b/src/HOL/Rings.thy	Fri Nov 13 12:27:13 2015 +0000
     1.3 @@ -1976,7 +1976,7 @@
     1.4    "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
     1.5    by (rule abs_eq_mult) auto
     1.6  
     1.7 -lemma abs_mult_self:
     1.8 +lemma abs_mult_self [simp]:
     1.9    "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
    1.10    by (simp add: abs_if)
    1.11