src/HOL/Arith.ML
changeset 3903 1b29151a1009
parent 3896 ee8ebb74ec00
child 3919 c036caebfc75
     1.1 --- a/src/HOL/Arith.ML	Thu Oct 16 15:09:08 1997 +0200
     1.2 +++ b/src/HOL/Arith.ML	Thu Oct 16 15:23:25 1997 +0200
     1.3 @@ -374,6 +374,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_le_self";
     1.7 +Addsimps [diff_le_self];
     1.8  
     1.9  goal Arith.thy "!!i::nat. i-j-k = i - (j+k)";
    1.10  by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
    1.11 @@ -604,9 +605,9 @@
    1.12  qed "Suc_diff_Suc";
    1.13  
    1.14  goal Arith.thy "!! i::nat. i <= n ==> n - (n - i) = i";
    1.15 -by (subgoal_tac "(n-i) + (n - (n-i)) = (n-i) + i" 1);
    1.16 -by (Full_simp_tac 1);
    1.17 -by (asm_simp_tac (!simpset addsimps [diff_le_self, add_commute]) 1);
    1.18 +by (etac rev_mp 1);
    1.19 +by (res_inst_tac [("m","n"),("n","i")] diff_induct 1);
    1.20 +by (ALLGOALS (asm_simp_tac  (!simpset addsimps [Suc_diff_le])));
    1.21  qed "diff_diff_cancel";
    1.22  Addsimps [diff_diff_cancel];
    1.23