1.1 --- a/src/HOL/Import/HOL_Light/HOLLightInt.thy	Tue Mar 27 14:49:56 2012 +0200
     1.2 +++ b/src/HOL/Import/HOL_Light/HOLLightInt.thy	Tue Mar 27 15:27:49 2012 +0200
     1.3 @@ -162,7 +162,7 @@
     1.4    apply (simp add: hl_mod_def hl_div_def)
     1.5    apply (metis comm_semiring_1_class.normalizing_semiring_rules(24) div_mult_self2 not_less_iff_gr_or_eq order_less_le add_0 zdiv_eq_0_iff mult_commute)
     1.6    apply (simp add: hl_mod_def hl_div_def)
     1.7 -  by (metis add.comm_neutral add_pos_nonneg div_mult_self1 less_minus_iff minus_add minus_add_cancel minus_minus mult_zero_right not_square_less_zero zdiv_eq_0_iff zdiv_zminus2)
     1.8 +  by (metis add.comm_neutral add_pos_nonneg div_mult_self1 less_minus_iff minus_add minus_add_cancel minus_minus mult_zero_right not_square_less_zero zdiv_eq_0_iff div_minus_right)
     1.9  
    1.10  lemma DEF_rem:
    1.11    "hl_mod = (SOME r. \<forall>m n. if n = int 0 then
    1.12 @@ -182,7 +182,7 @@
    1.13    apply (simp add: hl_mod_def hl_div_def)
    1.14    apply (metis add_left_cancel mod_div_equality)
    1.15    apply (simp add: hl_mod_def hl_div_def)
    1.16 -  by (metis minus_mult_right mod_mult_self2 mod_pos_pos_trivial add_commute zminus_zmod zmod_zminus2 mult_commute)
    1.17 +  by (metis minus_mult_right mod_mult_self2 mod_pos_pos_trivial add_commute zminus_zmod mod_minus_right mult_commute)
    1.18  
    1.19  lemma DEF_int_gcd:
    1.20    "int_gcd = (SOME d. \<forall>a b. (int 0) \<le> (d (a, b)) \<and> (d (a, b)) dvd a \<and>