# HG changeset patch
# User paulson
# Date 958136445 -7200
# Node ID 6bbb93189de60612ae8bcd5b65e2aa7d857181da
# Parent  b1ea21d70c856c81f1efa9a9d63d3e6279348497
tidied

diff -r b1ea21d70c85 -r 6bbb93189de6 src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Fri May 12 14:59:12 2000 +0200
+++ b/src/HOL/Divides.ML	Fri May 12 15:00:45 2000 +0200
@@ -285,17 +285,15 @@
 
 Goal "0<n ==> Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
 by (res_inst_tac [("n","m")] less_induct 1);
-by (excluded_middle_tac "Suc(na)<n" 1);
+by (case_tac "Suc(na)<n" 1);
 (* case Suc(na) < n *)
-by (forward_tac [lessI RS less_trans] 2);
-by (asm_simp_tac (simpset() addsimps [less_not_refl3]) 2);
+by (forward_tac [lessI RS less_trans] 1 
+    THEN asm_simp_tac (simpset() addsimps [less_not_refl3]) 1);
 (* case n <= Suc(na) *)
 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, le_Suc_eq, 
 					   mod_geq]) 1);
-by (etac disjE 1);
- by (Asm_simp_tac 2);
-by (asm_simp_tac (simpset() addsimps [Suc_diff_le, diff_less, 
-				      le_mod_geq]) 1);
+by (auto_tac (claset(), 
+	      simpset() addsimps [Suc_diff_le, diff_less, le_mod_geq]));
 qed "mod_Suc";
 
 Goal "0<n ==> m mod n < n";