src/HOL/Divides.thy
changeset 14208 144f45277d5a
parent 14131 a4fc8b1af5e7
child 14267 b963e9cee2a0
     1.1 --- a/src/HOL/Divides.thy	Fri Sep 26 10:34:28 2003 +0200
     1.2 +++ b/src/HOL/Divides.thy	Fri Sep 26 10:34:57 2003 +0200
     1.3 @@ -90,8 +90,7 @@
     1.4    "0 < n \<Longrightarrow> (n * q <= m \<and> m < n * (Suc q)) = (q = ((m::nat) div n))"
     1.5    apply (rule iffI)
     1.6    apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
     1.7 -  apply (simp_all add: quorem_def)
     1.8 -  apply arith
     1.9 +  apply (simp_all add: quorem_def, 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]])
    1.13 @@ -99,8 +98,7 @@
    1.14    apply (rule_tac P="%x. x < n + n * (m div n)" in
    1.15      subst [OF mod_div_equality [of _ n]])
    1.16    apply (simp only: add: mult_ac add_ac)
    1.17 -  apply (rule add_less_mono1)
    1.18 -  apply simp
    1.19 +  apply (rule add_less_mono1, simp)
    1.20    done
    1.21  
    1.22  theorem split_div':