src/HOL/Ring_and_Field.thy

 done
 
 lemma abs_idempotent [simp]: "abs (abs a) = abs (a::'a::ordered_ring)"
   by (force elim: order_less_asym simp add: abs_if)
 
-lemma abs_zero_iff [iff]: "(abs a = 0) = (a = (0::'a::ordered_ring))"
+lemma abs_zero_iff [simp]: "(abs a = 0) = (a = (0::'a::ordered_ring))"
 by (simp add: abs_if)
 
 lemma abs_ge_self: "a \<le> abs (a::'a::ordered_ring)"
 apply (simp add: abs_if)
 apply (simp add: order_less_imp_le order_trans [of _ 0])