| changeset 10964 | afc1dfc5a92d |
| parent 10789 | 260fa2c67e3e |
| child 11313 | 04c8da2e0917 |
--- 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 *)