src/HOL/Divides.ML
changeset 5498 7b81cae2774f
parent 5415 13a199e94877
child 5537 c2bd39a2c0ee
--- 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";