Got rid of some preds and replaced some n~=0 by 0<n.
authornipkow
Sat Dec 06 17:05:41 1997 +0100 (1997-12-06)
changeset 4378e52f864c5b88
parent 4377 2cba48b0f1c4
child 4379 7049ca8f912e
Got rid of some preds and replaced some n~=0 by 0<n.
src/HOL/Arith.ML
     1.1 --- a/src/HOL/Arith.ML	Sat Dec 06 16:48:39 1997 +0100
     1.2 +++ b/src/HOL/Arith.ML	Sat Dec 06 17:05:41 1997 +0100
     1.3 @@ -117,7 +117,7 @@
     1.4  Addsimps [pred_add_is_0];
     1.5  
     1.6  (* Could be generalized, eg to "!!n. k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
     1.7 -goal Arith.thy "!!n. n ~= 0 ==> m + pred n = pred(m+n)";
     1.8 +goal Arith.thy "!!n. 0<n ==> m + (n-1) = (m+n)-1";
     1.9  by (exhaust_tac "m" 1);
    1.10  by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc]
    1.11                                        addsplits [expand_nat_case])));