src/HOL/Divides.thy
changeset 20432 07ec57376051
parent 20380 14f9f2a1caa6
child 20589 24ecf9bc1a0a
     1.1 --- a/src/HOL/Divides.thy	Tue Aug 29 21:43:34 2006 +0200
     1.2 +++ b/src/HOL/Divides.thy	Wed Aug 30 03:19:08 2006 +0200
     1.3 @@ -710,7 +710,7 @@
     1.4    apply (rule iffI)
     1.5    apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
     1.6  prefer 3; apply assumption
     1.7 -  apply (simp_all add: quorem_def)
     1.8 +  apply (simp_all add: quorem_def) apply arith
     1.9    apply (rule conjI)
    1.10    apply (rule_tac P="%x. n * (m div n) \<le> x" in
    1.11      subst [OF mod_div_equality [of _ n]])