# HG changeset patch
# User paulson
# Date 956066201 -7200
# Node ID fa6c4e4182d9a9f33aa80a4a50f95e35af495c01
# Parent  60a1ed9e3c343b5eaef6ecb1b9db1369bc1ab3ac
replaced obsolete diff_right_cancel by diff_diff_eq

diff -r 60a1ed9e3c34 -r fa6c4e4182d9 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Tue Apr 18 15:54:56 2000 +0200
+++ b/src/HOL/Arith.ML	Tue Apr 18 15:56:41 2000 +0200
@@ -1107,6 +1107,11 @@
 by (arith_tac 1);
 qed "diff_less";
 
+Goal "j <= (k::nat) ==> (j+i)-k = i-(k-j)";
+by (asm_simp_tac (simpset() addsplits [nat_diff_split']) 1);
+qed "diff_add_assoc_diff";
+
+
 (*** Reducing subtraction to addition ***)
 
 Goal "n<=(l::nat) --> Suc l - n + m = Suc (l - n + m)";
@@ -1125,11 +1130,11 @@
 by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
 qed "diff_Suc_le_Suc_diff";
 
-Goal "[| k<=n; n<=m |] ==> (m-k) - (n-k) = m-(n::nat)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_right_cancel";
+(** Simplification of relational expressions involving subtraction **)
 
-(** Simplification of relational expressions involving subtraction **)
+Goal "[| k <= m;  k <= (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)";
+by (asm_simp_tac (simpset() addsplits [nat_diff_split']) 1);
+qed "diff_diff_eq";
 
 Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k = n-k) = (m=n)";
 by (auto_tac (claset(), simpset() addsplits [nat_diff_split']));