src/HOL/arith_data.ML
changeset 5429 0833486c23ce
parent 5418 a895ab904b85
child 5553 ae42b36a50c2
     1.1 --- a/src/HOL/arith_data.ML	Fri Sep 04 13:24:10 1998 +0200
     1.2 +++ b/src/HOL/arith_data.ML	Mon Sep 07 10:40:17 1998 +0200
     1.3 @@ -222,13 +222,13 @@
     1.4  
     1.5  
     1.6  (*This proof requires natdiff_cancel_sums*)
     1.7 -goal Arith.thy "!!n::nat. m<n --> m<l --> (l-n) < (l-m)";
     1.8 +Goal "m < (n::nat) --> m<l --> (l-n) < (l-m)";
     1.9  by (induct_tac "l" 1);
    1.10  by (Simp_tac 1);
    1.11  by (Clarify_tac 1);
    1.12  by (etac less_SucE 1);
    1.13 +by (Clarify_tac 2);
    1.14 +by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 2);
    1.15  by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
    1.16  				      Suc_diff_le]) 1);
    1.17 -by (Clarify_tac 1);
    1.18 -by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 1);
    1.19  qed_spec_mp "diff_less_mono2";