src/HOL/Arith.ML
changeset 3896 ee8ebb74ec00
parent 3842 b55686a7b22c
child 3903 1b29151a1009
     1.1 --- a/src/HOL/Arith.ML	Thu Oct 16 14:00:20 1997 +0200
     1.2 +++ b/src/HOL/Arith.ML	Thu Oct 16 14:12:15 1997 +0200
     1.3 @@ -38,6 +38,12 @@
     1.4  by(simp_tac (!simpset setloop (split_tac[expand_nat_case])) 1);
     1.5  qed_spec_mp "pred_le_mono";
     1.6  
     1.7 +goal Arith.thy "!!n. n ~= 0 ==> pred n < n";
     1.8 +by(exhaust_tac "n" 1);
     1.9 +by(ALLGOALS Asm_full_simp_tac);
    1.10 +qed "pred_less";
    1.11 +Addsimps [pred_less];
    1.12 +
    1.13  (** Difference **)
    1.14  
    1.15  qed_goalw "diff_0_eq_0" Arith.thy [pred_def]