# HG changeset patch
# User wenzelm
# Date 1201125429 -3600
# Node ID 1f2f4d941e9eae7b6d9e783cc90a28038c7fb96b
# Parent  8ceff6c1f2a83f47b5777fda74a9cc049cd896a8
tuned proofs;

diff -r 8ceff6c1f2a8 -r 1f2f4d941e9e src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Jan 23 22:57:07 2008 +0100
+++ b/src/HOL/Divides.thy	Wed Jan 23 22:57:09 2008 +0100
@@ -160,14 +160,14 @@
   fix n m :: nat
   show "(m div n) * n + m mod n = m"
     apply (cases "n = 0", simp)
-    apply (induct m rule: nat_less_induct [rule_format])
+    apply (induct m rule: less_induct)
     apply (subst mod_if)
     apply (simp add: add_assoc add_diff_inverse le_div_geq)
     done
 next
   fix n :: nat
   show "n div 0 = 0"
-    by (rule div_eq [THEN wf_less_trans], simp)
+    by (rule div_eq [THEN wf_less_trans]) simp
 next
   fix n m :: nat
   assume "n \<noteq> 0"