# HG changeset patch
# User paulson
# Date 906122196 -7200
# Node ID 7b81cae2774fa88af4cd81a9a940a92eaea86dd0
# Parent  497215d66441e1b73a270176a1a2e736946ea555
tidying

diff -r 497215d66441 -r 7b81cae2774f src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Fri Sep 18 14:36:03 1998 +0200
+++ b/src/HOL/Divides.ML	Fri Sep 18 14:36:36 1998 +0200
@@ -257,11 +257,11 @@
 
 Goal "0<n ==> m mod n < n";
 by (res_inst_tac [("n","m")] less_induct 1);
-by (excluded_middle_tac "na<n" 1);
+by (case_tac "na<n" 1);
+(*case n le na*)
+by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 2);
 (*case na<n*)
-by (asm_simp_tac (simpset() addsimps [mod_less]) 2);
-(*case n le na*)
-by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 1);
+by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
 qed "mod_less_divisor";
 
 
@@ -306,9 +306,9 @@
 qed "mod2_add_self";
 Addsimps [mod2_add_self];
 
+(*Restore the default*)
 Delrules [less_SucE];
 
-
 (*** More division laws ***)
 
 Goal "0<n ==> m*n div n = m";