--- a/src/HOL/Divides.ML Mon Sep 06 18:18:23 1999 +0200
+++ b/src/HOL/Divides.ML Mon Sep 06 18:18:30 1999 +0200
@@ -437,6 +437,17 @@
(* k dvd (m*k) *)
AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
+Goal "k dvd (n + k) = k dvd (n::nat)";
+br iffI 1;
+be dvd_add 2;
+br dvd_refl 2;
+by (subgoal_tac "n = (n+k)-k" 1);
+by (Simp_tac 2);
+be ssubst 1;
+be dvd_diff 1;
+br dvd_refl 1;
+qed "dvd_reduce";
+
Goalw [dvd_def] "[| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
by (Clarify_tac 1);
by (Full_simp_tac 1);