1.1 --- a/src/HOL/Arith.ML	Tue Aug 18 10:27:14 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Wed Aug 19 10:26:02 1998 +0200
     1.3 @@ -375,7 +375,7 @@
     1.4  by (asm_simp_tac (simpset() addsimps [Suc_diff_n]) 1);
     1.5  qed "diff_Suc_less_diff";
     1.6  
     1.7 -Goal "!!n::nat. m - n <= Suc m - n";
     1.8 +Goal "m - n <= Suc m - n";
     1.9  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.10  by (ALLGOALS Asm_simp_tac);
    1.11  qed "diff_le_Suc_diff";
    1.12 @@ -429,20 +429,20 @@
    1.13  by (REPEAT(Simp_tac 1 THEN TRY(atac 1)));
    1.14  qed_spec_mp "diffs0_imp_equal";
    1.15  
    1.16 -Goal "m<n ==> 0<n-m";
    1.17 -by (etac rev_mp 1);
    1.18 +Goal "(0<n-m) = (m<n)";
    1.19  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.20  by (ALLGOALS Asm_simp_tac);
    1.21 -qed "less_imp_diff_positive";
    1.22 +qed "zero_less_diff";
    1.23 +Addsimps [zero_less_diff];
    1.24  
    1.25 -Goal "!! (i::nat). i < j  ==> ? k. 0<k & i+k = j";
    1.26 +Goal "i < j  ==> ? k. 0<k & i+k = j";
    1.27  by (res_inst_tac [("x","j - i")] exI 1);
    1.28 -by (fast_tac (claset() addDs [less_trans, less_irrefl] 
    1.29 -   	               addIs [less_imp_diff_positive, add_diff_inverse]) 1);
    1.30 +by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1);
    1.31  qed "less_imp_add_positive";
    1.32  
    1.33  Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
    1.34 -by (simp_tac (simpset() addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]) 1);
    1.35 +by (simp_tac (simpset() addsimps [less_imp_diff_is_0,
    1.36 +				  not_less_eq, Suc_diff_n]) 1);
    1.37  qed "if_Suc_diff_n";
    1.38  
    1.39  Goal "Suc(m)-n <= Suc(m-n)";