author | nipkow |
Sat, 02 Jan 2010 21:31:15 +0100 | |
changeset 34225 | 21c5405deb6b |
parent 34223 | dce32a1e05fe |
child 34226 | aec597ef135c |
--- a/src/HOL/Divides.thy Fri Jan 01 19:15:43 2010 +0100 +++ b/src/HOL/Divides.thy Sat Jan 02 21:31:15 2010 +0100 @@ -2322,7 +2322,7 @@ text{*Suggested by Matthias Daum*} lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)" apply (subgoal_tac "nat x div nat k < nat x") - apply (simp (asm_lr) add: nat_div_distrib [symmetric]) + apply (simp add: nat_div_distrib [symmetric]) apply (rule Divides.div_less_dividend, simp_all) done