src/HOL/Divides.thy
changeset 34225 21c5405deb6b
parent 34126 8a2c5d7aff51
child 34982 7b8c366e34a2
     1.1 --- a/src/HOL/Divides.thy	Fri Jan 01 19:15:43 2010 +0100
     1.2 +++ b/src/HOL/Divides.thy	Sat Jan 02 21:31:15 2010 +0100
     1.3 @@ -2322,7 +2322,7 @@
     1.4  text{*Suggested by Matthias Daum*}
     1.5  lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
     1.6  apply (subgoal_tac "nat x div nat k < nat x")
     1.7 - apply (simp (asm_lr) add: nat_div_distrib [symmetric])
     1.8 + apply (simp add: nat_div_distrib [symmetric])
     1.9  apply (rule Divides.div_less_dividend, simp_all)
    1.10  done
    1.11