added "m <= n ==> m-n = 0" [simp]

--- a/src/HOL/Nat.ML	Fri Apr 19 14:51:33 2002 +0200
+++ b/src/HOL/Nat.ML	Thu Apr 25 17:36:29 2002 +0200
@@ -541,7 +541,7 @@
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "diff_is_0_eq";
-Addsimps [diff_is_0_eq];
+Addsimps [diff_is_0_eq, diff_is_0_eq RS iffD2];
 
 Goal "!!m::nat. (0<n-m) = (m<n)";
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);