src/HOL/Rings.thy
changeset 44921 58eef4843641
parent 44350 63cddfbc5a09
child 49962 a8cc904a6820
     1.1 --- a/src/HOL/Rings.thy	Tue Sep 13 08:21:51 2011 -0700
     1.2 +++ b/src/HOL/Rings.thy	Tue Sep 13 17:07:33 2011 -0700
     1.3 @@ -1100,7 +1100,7 @@
     1.4  
     1.5  lemma abs_one [simp]:
     1.6    "\<bar>1\<bar> = 1"
     1.7 -  by (simp add: abs_if zero_less_one [THEN less_not_sym])
     1.8 +  by (simp add: abs_if)
     1.9  
    1.10  end
    1.11