# HG changeset patch
# User nipkow
# Date 1262464293 -3600
# Node ID aec597ef135c501eec3d563bbcfa9ddfaa044dd0
# Parent  143e3dabec2b55147ec38b57ab008068dd9e0d38# Parent  21c5405deb6b49a0281a4afff3fcc7a736392167
merged

diff -r 143e3dabec2b -r aec597ef135c src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sat Jan 02 20:10:21 2010 +0100
+++ b/src/HOL/Divides.thy	Sat Jan 02 21:31:33 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