src/HOL/Divides.thy
changeset 64848 c50db2128048
parent 64785 ae0bbc8e45ad
child 65556 fcd599570afa
     1.1 --- a/src/HOL/Divides.thy	Mon Jan 09 15:54:48 2017 +0000
     1.2 +++ b/src/HOL/Divides.thy	Mon Jan 09 18:53:06 2017 +0100
     1.3 @@ -1812,7 +1812,7 @@
     1.4    assume "l \<noteq> 0"
     1.5    then show "k * l div l = k"
     1.6      by (auto simp add: eucl_rel_int_iff ac_simps intro: div_int_unique [of _ _ _ 0])
     1.7 -qed (simp_all add: sgn_mult mult_sgn_abs abs_sgn_eq)
     1.8 +qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
     1.9  
    1.10  end
    1.11