1.1 --- a/NEWS	Sun Mar 01 10:24:57 2009 +0100
     1.2 +++ b/NEWS	Sun Mar 01 12:01:57 2009 +0100
     1.3 @@ -385,6 +385,7 @@
     1.4  nat_mod_mod_trivial    -> mod_mod_trivial
     1.5  zdiv_zadd_self1        -> div_add_self1
     1.6  zdiv_zadd_self2        -> div_add_self2
     1.7 +zdiv_zmult_self1       -> div_mult_self2_is_id
     1.8  zdiv_zmult_self2       -> div_mult_self1_is_id
     1.9  zdvd_triv_left         -> dvd_triv_left
    1.10  zdvd_triv_right        -> dvd_triv_right

     2.1 --- a/src/HOL/IntDiv.thy	Sun Mar 01 10:24:57 2009 +0100
     2.2 +++ b/src/HOL/IntDiv.thy	Sun Mar 01 12:01:57 2009 +0100
     2.3 @@ -689,9 +689,6 @@
     2.4  apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_mod])
     2.5  done
     2.6  
     2.7 -lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
     2.8 -by (simp add: zdiv_zmult1_eq)
     2.9 -
    2.10  lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"
    2.11  apply (case_tac "b = 0", simp)
    2.12  apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
    2.13 @@ -717,7 +714,7 @@
    2.14    assume not0: "b \<noteq> 0"
    2.15    show "(a + c * b) div b = c + a div b"
    2.16      unfolding zdiv_zadd1_eq [of a "c * b"] using not0 
    2.17 -      by (simp add: zmod_zmult1_eq zmod_zdiv_trivial)
    2.18 +      by (simp add: zmod_zmult1_eq zmod_zdiv_trivial zdiv_zmult1_eq)
    2.19  qed auto
    2.20  
    2.21  lemma posDivAlg_div_mod:

     3.1 --- a/src/HOL/Library/Float.thy	Sun Mar 01 10:24:57 2009 +0100
     3.2 +++ b/src/HOL/Library/Float.thy	Sun Mar 01 12:01:57 2009 +0100
     3.3 @@ -1093,7 +1093,7 @@
     3.4    { have "2^(prec - 1) * m \<le> 2^(prec - 1) * 2^?b" using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono, auto)
     3.5      also have "\<dots> = 2 ^ nat (int prec + bitlen m - 1)" unfolding pow_split zpower_zadd_distrib by auto
     3.6      finally have "2^(prec - 1) * m div m \<le> 2 ^ nat (int prec + bitlen m - 1) div m" using `0 < m` by (rule zdiv_mono1)
     3.7 -    hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m" unfolding zdiv_zmult_self1[OF `m \<noteq> 0`] .
     3.8 +    hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m" unfolding div_mult_self2_is_id[OF `m \<noteq> 0`] .
     3.9      hence "2^(prec - 1) * inverse (2 ^ nat (int prec + bitlen m - 1)) \<le> ?d"
    3.10        unfolding real_of_int_le_iff[of "2^(prec - 1)", symmetric] by auto }
    3.11    from mult_left_mono[OF this[unfolded pow_split power_add inverse_mult_distrib real_mult_assoc[symmetric] right_inverse[OF pow_not0] real_mult_1], of "2^?e"]