src/HOL/Arith.ML
changeset 4378 e52f864c5b88
parent 4360 40e5c97e988d
child 4389 1865cb8df116
     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])));