src/HOL/Divides.thy
changeset 61649 268d88ec9087
parent 61433 a4c0de1df3d8
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Divides.thy	Thu Nov 12 11:22:26 2015 +0100
     1.2 +++ b/src/HOL/Divides.thy	Fri Nov 13 12:27:13 2015 +0000
     1.3 @@ -1696,17 +1696,14 @@
     1.4  
     1.5  lemma divmod_int_rel:
     1.6    "divmod_int_rel k l (k div l, k mod l)"
     1.7 +  unfolding divmod_int_rel_def divide_int_def mod_int_def
     1.8    apply (cases k rule: int_cases3)
     1.9 -  apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
    1.10 +  apply (simp add: mod_greater_zero_iff_not_dvd not_le algebra_simps)
    1.11    apply (cases l rule: int_cases3)
    1.12 -  apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
    1.13 -  apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
    1.14 -  apply (simp add: of_nat_add [symmetric])
    1.15 -  apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
    1.16 -  apply (simp add: of_nat_add [symmetric])
    1.17 +  apply (simp add: mod_greater_zero_iff_not_dvd not_le algebra_simps)
    1.18 +  apply (simp_all del: of_nat_add of_nat_mult add: mod_greater_zero_iff_not_dvd not_le algebra_simps int_dvd_iff of_nat_add [symmetric] of_nat_mult [symmetric])
    1.19    apply (cases l rule: int_cases3)
    1.20 -  apply (simp_all add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
    1.21 -  apply (simp_all add: of_nat_add [symmetric])
    1.22 +  apply (simp_all del: of_nat_add of_nat_mult add: not_le algebra_simps int_dvd_iff of_nat_add [symmetric] of_nat_mult [symmetric])
    1.23    done
    1.24  
    1.25  instantiation int :: ring_div