# HG changeset patch
# User nipkow
# Date 915900954 -3600
# Node ID c148037f53c681c5ebbcb286080aafe72f1f16d7
# Parent  34242451bc9104d47a152584ecc1d1d76fcd8beb
Remoaved a few now redundant rewrite rules.

diff -r 34242451bc91 -r c148037f53c6 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Sat Jan 09 15:25:44 1999 +0100
+++ b/src/HOL/Arith.ML	Sat Jan 09 17:55:54 1999 +0100
@@ -124,12 +124,12 @@
 by (exhaust_tac "m" 1);
 by (ALLGOALS (fast_tac (claset() addss (simpset()))));
 qed "pred_add_is_0";
-Addsimps [pred_add_is_0];
+(*Addsimps [pred_add_is_0];*)
 
 (* Could be generalized, eg to "k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
 Goal "0<n ==> m + (n-1) = (m+n)-1";
 by (exhaust_tac "m" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc]
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc, Suc_n_not_n]
                                       addsplits [nat.split])));
 qed "add_pred";
 Addsimps [add_pred];
@@ -365,7 +365,7 @@
 
 Goal "m - n <= (m::nat)";
 by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [le_SucI])));
 qed "diff_le_self";
 Addsimps [diff_le_self];
 
@@ -929,8 +929,7 @@
 fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.boolT);
 
 val pats = map prep_pat
-  ["(m::nat) < n","(m::nat) <= n", "~ (m::nat) < n","~ (m::nat) <= n",
-   "(m::nat) = n"]
+  ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"]
 
 in
 val fast_nat_arith_simproc =
diff -r 34242451bc91 -r c148037f53c6 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Sat Jan 09 15:25:44 1999 +0100
+++ b/src/HOL/NatDef.ML	Sat Jan 09 17:55:54 1999 +0100
@@ -283,7 +283,7 @@
 Goal "~(Suc(n) < n)";
 by (blast_tac (claset() addEs [Suc_lessD RS less_irrefl]) 1);
 qed "not_Suc_n_less_n";
-Addsimps [not_Suc_n_less_n];
+(*Addsimps [not_Suc_n_less_n];*)
 
 Goal "i<j ==> j<k --> Suc i < k";
 by (nat_ind_tac "k" 1);
@@ -318,6 +318,7 @@
 Goalw [le_def] "0 <= n";
 by (rtac not_less0 1);
 qed "le0";
+AddIffs [le0];
 
 Goalw [le_def] "~ Suc n <= n";
 by (Simp_tac 1);
@@ -329,10 +330,6 @@
 qed "le_0_eq";
 AddIffs [le_0_eq];
 
-Addsimps [(*less_Suc_eq, makes simpset non-confluent*) le0, le_0_eq,
-          Suc_n_not_le_n,
-          n_not_Suc_n, Suc_n_not_n];
-
 Goal "(m <= Suc(n)) = (m<=n | m = Suc n)";
 by (simp_tac (simpset() delsimps [less_Suc_eq_le]
 			addsimps [less_Suc_eq_le RS sym, less_Suc_eq]) 1);