src/HOL/Arith.ML
changeset 5604 cd17004d09e1
parent 5598 6b8dee1a6ebb
child 5654 8b872d546b9e
     1.1 --- a/src/HOL/Arith.ML	Thu Oct 01 20:33:01 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Fri Oct 02 10:41:35 1998 +0200
     1.3 @@ -146,7 +146,7 @@
     1.4  (*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
     1.5  Goal "m<n --> (? k. n=Suc(m+k))";
     1.6  by (induct_tac "n" 1);
     1.7 -by (ALLGOALS (simp_tac (simpset() addsimps [le_eq_less_or_eq])));
     1.8 +by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less])));
     1.9  by (blast_tac (claset() addSEs [less_SucE] 
    1.10                          addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
    1.11  qed_spec_mp "less_eq_Suc_add";
    1.12 @@ -245,7 +245,7 @@
    1.13  \        i <= j                                 \
    1.14  \     |] ==> f(i) <= (f(j)::nat)";
    1.15  by (cut_facts_tac [le] 1);
    1.16 -by (asm_full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
    1.17 +by (asm_full_simp_tac (simpset() addsimps [order_le_less]) 1);
    1.18  by (blast_tac (claset() addSIs [lt_mono]) 1);
    1.19  qed "less_mono_imp_le_mono";
    1.20  
    1.21 @@ -397,11 +397,6 @@
    1.22  	      simpset() addsimps [Suc_diff_le]@le_simps));
    1.23  qed "diff_Suc_less_diff";
    1.24  
    1.25 -Goal "m - n <= Suc m - n";
    1.26 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.27 -by (ALLGOALS Asm_simp_tac);
    1.28 -qed "diff_le_Suc_diff";
    1.29 -
    1.30  (*This and the next few suggested by Florian Kammueller*)
    1.31  Goal "!!i::nat. i-j-k = i-k-j";
    1.32  by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1);
    1.33 @@ -702,7 +697,7 @@
    1.34  Goal "n - Suc i <= n - i";
    1.35  by (case_tac "i<n" 1);
    1.36  by (dtac diff_Suc_less_diff 1);
    1.37 -by (auto_tac (claset(), simpset() addsimps [leI]));
    1.38 +by (auto_tac (claset(), simpset() addsimps [less_imp_le, leI]));
    1.39  qed "diff_Suc_le_diff";
    1.40  AddIffs [diff_Suc_le_diff];
    1.41