# HG changeset patch
# User paulson
# Date 980261256 -3600
# Node ID afc1dfc5a92d6c153d957164520c2c16bc46fcf0
# Parent  f2c1a280f1e3921de0ad0cda0ebb242f24bc601e
the 0<n premise was unnecessary

diff -r f2c1a280f1e3 -r afc1dfc5a92d src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Tue Jan 23 15:46:25 2001 +0100
+++ b/src/HOL/Divides.ML	Tue Jan 23 15:47:36 2001 +0100
@@ -486,7 +486,8 @@
 
 (*** Further facts about mod (mainly for the mutilated chess board ***)
 
-Goal "0<n ==> Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
+Goal "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
+by (div_undefined_case_tac "n=0" 1);
 by (induct_thm_tac nat_less_induct "m" 1);
 by (case_tac "Suc(na)<n" 1);
 (* case Suc(na) < n *)