src/HOL/Nat.ML
changeset 13094 643fce75f6cd
parent 12949 b94843ffc0d1
child 13438 527811f00c56
     1.1 --- a/src/HOL/Nat.ML	Fri Apr 19 14:51:33 2002 +0200
     1.2 +++ b/src/HOL/Nat.ML	Thu Apr 25 17:36:29 2002 +0200
     1.3 @@ -541,7 +541,7 @@
     1.4  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
     1.5  by (ALLGOALS Asm_simp_tac);
     1.6  qed "diff_is_0_eq";
     1.7 -Addsimps [diff_is_0_eq];
     1.8 +Addsimps [diff_is_0_eq, diff_is_0_eq RS iffD2];
     1.9  
    1.10  Goal "!!m::nat. (0<n-m) = (m<n)";
    1.11  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);