| changeset 13094 | 643fce75f6cd |
| parent 12949 | b94843ffc0d1 |
| child 13438 | 527811f00c56 |
--- 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);