src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Divides.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -710,8 +710,7 @@
   apply (rule iffI)
   apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
 prefer 3; apply assumption
-  apply (simp_all add: quorem_def)
-  apply arith
+  apply (simp_all add: quorem_def) apply arith
   apply (rule conjI)
   apply (rule_tac P="%x. n * (m div n) \<le> x" in
     subst [OF mod_div_equality [of _ n]])