tuned proofs;
authorwenzelm
Wed Jan 23 22:57:09 2008 +0100 (2008-01-23)
changeset 259471f2f4d941e9e
parent 25946 8ceff6c1f2a8
child 25948 aa65ada6f095
tuned proofs;
src/HOL/Divides.thy
     1.1 --- a/src/HOL/Divides.thy	Wed Jan 23 22:57:07 2008 +0100
     1.2 +++ b/src/HOL/Divides.thy	Wed Jan 23 22:57:09 2008 +0100
     1.3 @@ -160,14 +160,14 @@
     1.4    fix n m :: nat
     1.5    show "(m div n) * n + m mod n = m"
     1.6      apply (cases "n = 0", simp)
     1.7 -    apply (induct m rule: nat_less_induct [rule_format])
     1.8 +    apply (induct m rule: less_induct)
     1.9      apply (subst mod_if)
    1.10      apply (simp add: add_assoc add_diff_inverse le_div_geq)
    1.11      done
    1.12  next
    1.13    fix n :: nat
    1.14    show "n div 0 = 0"
    1.15 -    by (rule div_eq [THEN wf_less_trans], simp)
    1.16 +    by (rule div_eq [THEN wf_less_trans]) simp
    1.17  next
    1.18    fix n m :: nat
    1.19    assume "n \<noteq> 0"