# HG changeset patch
# User nipkow
# Date 1019748989 -7200
# Node ID 643fce75f6cddb9e3ea91968a73a7988cc8540cc
# Parent  ab033530790541677e622fb4f134b9f0fb57f0b2
added "m <= n ==> m-n = 0" [simp]

diff -r ab0335307905 -r 643fce75f6cd src/HOL/Nat.ML
--- 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);