# HG changeset patch
# User nipkow
# Date 881424341 -3600
# Node ID e52f864c5b884ff465244d2d472a0a981342e6f2
# Parent  2cba48b0f1c4e5e564465fab9f86092949b79d97
Got rid of some preds and replaced some n~=0 by 0<n.

diff -r 2cba48b0f1c4 -r e52f864c5b88 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Sat Dec 06 16:48:39 1997 +0100
+++ b/src/HOL/Arith.ML	Sat Dec 06 17:05:41 1997 +0100
@@ -117,7 +117,7 @@
 Addsimps [pred_add_is_0];
 
 (* Could be generalized, eg to "!!n. k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
-goal Arith.thy "!!n. n ~= 0 ==> m + pred n = pred(m+n)";
+goal Arith.thy "!!n. 0<n ==> m + (n-1) = (m+n)-1";
 by (exhaust_tac "m" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc]
                                       addsplits [expand_nat_case])));