# HG changeset patch
# User paulson
# Date 907317695 -7200
# Node ID cd17004d09e1adebe40ca2513bc060fd0af41fe7
# Parent  12152ce11ce1638bf9fa7567d7aa9d4775cbc518
tidying

diff -r 12152ce11ce1 -r cd17004d09e1 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Thu Oct 01 20:33:01 1998 +0200
+++ b/src/HOL/Arith.ML	Fri Oct 02 10:41:35 1998 +0200
@@ -146,7 +146,7 @@
 (*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
 Goal "m<n --> (? k. n=Suc(m+k))";
 by (induct_tac "n" 1);
-by (ALLGOALS (simp_tac (simpset() addsimps [le_eq_less_or_eq])));
+by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less])));
 by (blast_tac (claset() addSEs [less_SucE] 
                         addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
 qed_spec_mp "less_eq_Suc_add";
@@ -245,7 +245,7 @@
 \        i <= j                                 \
 \     |] ==> f(i) <= (f(j)::nat)";
 by (cut_facts_tac [le] 1);
-by (asm_full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
+by (asm_full_simp_tac (simpset() addsimps [order_le_less]) 1);
 by (blast_tac (claset() addSIs [lt_mono]) 1);
 qed "less_mono_imp_le_mono";
 
@@ -397,11 +397,6 @@
 	      simpset() addsimps [Suc_diff_le]@le_simps));
 qed "diff_Suc_less_diff";
 
-Goal "m - n <= Suc m - n";
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "diff_le_Suc_diff";
-
 (*This and the next few suggested by Florian Kammueller*)
 Goal "!!i::nat. i-j-k = i-k-j";
 by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1);
@@ -702,7 +697,7 @@
 Goal "n - Suc i <= n - i";
 by (case_tac "i<n" 1);
 by (dtac diff_Suc_less_diff 1);
-by (auto_tac (claset(), simpset() addsimps [leI]));
+by (auto_tac (claset(), simpset() addsimps [less_imp_le, leI]));
 qed "diff_Suc_le_diff";
 AddIffs [diff_Suc_le_diff];