diff -r 9be357df93d4 -r af44242c5e7a src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Fri Feb 18 15:20:44 2000 +0100
+++ b/src/HOL/Arith.ML	Fri Feb 18 15:28:32 2000 +0100
@@ -1006,8 +1006,7 @@
 simpset_ref () := (simpset() addSolver
    (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac));
 
-(*Elimination of `-' on nat due to John Harrison.  An alternative is to
-  replace b=a+d by a<b; not clear that it makes much difference. *)
+(*Elimination of `-' on nat due to John Harrison. *)
 Goal "P(a - b::nat) = (ALL d. (b = a + d --> P 0) & (a = b + d --> P d))";
 by (case_tac "a <= b" 1);
 by Auto_tac;
@@ -1015,6 +1014,11 @@
 by (asm_simp_tac (simpset() addsimps [diff_is_0_eq RS iffD2]) 1);
 qed "nat_diff_split";
 
+(*LCP's version, replacing b=a+d by a<b, which sometimes works better*)
+Goal "P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))";
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
+qed "nat_diff_split'";
+
 
 (* FIXME: K true should be replaced by a sensible test to speed things up
    in case there are lots of irrelevant terms involved;