# HG changeset patch
# User paulson
# Date 877008205 -7200
# Node ID 1b29151a100995157d42583715fcb49e70da0015
# Parent  265a5d8ab88fb4cc57733c6d05064bbea8ae1176
New simprule diff_le_self, requiring a new proof of diff_diff_cancel

diff -r 265a5d8ab88f -r 1b29151a1009 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Thu Oct 16 15:09:08 1997 +0200
+++ b/src/HOL/Arith.ML	Thu Oct 16 15:23:25 1997 +0200
@@ -374,6 +374,7 @@
 by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "diff_le_self";
+Addsimps [diff_le_self];
 
 goal Arith.thy "!!i::nat. i-j-k = i - (j+k)";
 by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
@@ -604,9 +605,9 @@
 qed "Suc_diff_Suc";
 
 goal Arith.thy "!! i::nat. i <= n ==> n - (n - i) = i";
-by (subgoal_tac "(n-i) + (n - (n-i)) = (n-i) + i" 1);
-by (Full_simp_tac 1);
-by (asm_simp_tac (!simpset addsimps [diff_le_self, add_commute]) 1);
+by (etac rev_mp 1);
+by (res_inst_tac [("m","n"),("n","i")] diff_induct 1);
+by (ALLGOALS (asm_simp_tac  (!simpset addsimps [Suc_diff_le])));
 qed "diff_diff_cancel";
 Addsimps [diff_diff_cancel];