src/HOL/Divides.thy
changeset 44766 d4d33a4d7548
parent 43594 ef1ddc59b825
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Divides.thy	Tue Sep 06 16:30:39 2011 -0700
     1.2 +++ b/src/HOL/Divides.thy	Tue Sep 06 19:03:41 2011 -0700
     1.3 @@ -1732,16 +1732,16 @@
     1.4      1 div z and 1 mod z **)
     1.5  
     1.6  lemmas div_pos_pos_1_number_of [simp] =
     1.7 -    div_pos_pos [OF int_0_less_1, of "number_of w", standard]
     1.8 +    div_pos_pos [OF zero_less_one, of "number_of w", standard]
     1.9  
    1.10  lemmas div_pos_neg_1_number_of [simp] =
    1.11 -    div_pos_neg [OF int_0_less_1, of "number_of w", standard]
    1.12 +    div_pos_neg [OF zero_less_one, of "number_of w", standard]
    1.13  
    1.14  lemmas mod_pos_pos_1_number_of [simp] =
    1.15 -    mod_pos_pos [OF int_0_less_1, of "number_of w", standard]
    1.16 +    mod_pos_pos [OF zero_less_one, of "number_of w", standard]
    1.17  
    1.18  lemmas mod_pos_neg_1_number_of [simp] =
    1.19 -    mod_pos_neg [OF int_0_less_1, of "number_of w", standard]
    1.20 +    mod_pos_neg [OF zero_less_one, of "number_of w", standard]
    1.21  
    1.22  
    1.23  lemmas posDivAlg_eqn_1_number_of [simp] =
    1.24 @@ -1790,7 +1790,7 @@
    1.25  apply (subgoal_tac "b*q = r' - r + b'*q'")
    1.26   prefer 2 apply simp
    1.27  apply (simp (no_asm_simp) add: right_distrib)
    1.28 -apply (subst add_commute, rule zadd_zless_mono, arith)
    1.29 +apply (subst add_commute, rule add_less_le_mono, arith)
    1.30  apply (rule mult_right_mono, auto)
    1.31  done
    1.32