src/HOL/Divides.thy
changeset 20217 25b068a99d2b
parent 20044 92cc2f4c7335
child 20254 58b71535ed00
     1.1 --- a/src/HOL/Divides.thy	Wed Jul 26 13:31:07 2006 +0200
     1.2 +++ b/src/HOL/Divides.thy	Wed Jul 26 19:23:04 2006 +0200
     1.3 @@ -710,8 +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 arith
     1.9 +  apply (simp_all add: quorem_def) apply arith
    1.10    apply (rule conjI)
    1.11    apply (rule_tac P="%x. n * (m div n) \<le> x" in
    1.12      subst [OF mod_div_equality [of _ n]])