Refined arithmetic.

--- a/src/HOL/Arith.ML	Wed Jan 13 12:08:51 1999 +0100
+++ b/src/HOL/Arith.ML	Wed Jan 13 12:16:34 1999 +0100
@@ -966,7 +966,7 @@
 *)
 val nat_arith_tac =
   refute_tac (K true) (REPEAT o split_tac[nat_diff_split])
-             ((REPEAT o etac nat_neqE) THEN' fast_nat_arith_tac);
+             ((REPEAT_DETERM o etac nat_neqE) THEN' fast_nat_arith_tac);
 
 (*---------------------------------------------------------------------------*)
 (* End of proof procedures. Now go and USE them!                             *)

--- a/src/HOL/Integ/IntDef.ML	Wed Jan 13 12:08:51 1999 +0100
+++ b/src/HOL/Integ/IntDef.ML	Wed Jan 13 12:16:34 1999 +0100
@@ -533,8 +533,6 @@
 by (simp_tac (simpset() addsimps [integ_le_less]) 1);
 qed "zle_refl";
 
-AddIffs [le_refl];
-
 Goalw [zle_def] "z < w ==> z <= (w::int)";
 by (blast_tac (claset() addEs [zless_asym]) 1);
 qed "zless_imp_zle";

--- a/src/HOL/Nat.ML	Wed Jan 13 12:08:51 1999 +0100
+++ b/src/HOL/Nat.ML	Wed Jan 13 12:16:34 1999 +0100
@@ -54,12 +54,6 @@
 qed "not_gr0";
 AddIffs [not_gr0];
 
-(*Goal "m<n ==> 0 < n";
-by (dtac gr_implies_not0 1);
-by (Asm_full_simp_tac 1);
-qed "gr_implies_gr0";
-Addsimps [gr_implies_gr0];*)
-
 qed_goalw "Least_Suc" thy [Least_nat_def]
  "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
  (fn _ => [

--- a/src/HOL/NatDef.ML	Wed Jan 13 12:08:51 1999 +0100
+++ b/src/HOL/NatDef.ML	Wed Jan 13 12:16:34 1999 +0100
@@ -418,8 +418,6 @@
 by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
 qed "le_refl";
 
-AddIffs [le_refl];
-
 
 Goal "[| i <= j; j < k |] ==> i < (k::nat)";
 by (blast_tac (claset() addSDs [le_imp_less_or_eq]

--- a/src/HOL/Ord.ML	Wed Jan 13 12:08:51 1999 +0100
+++ b/src/HOL/Ord.ML	Wed Jan 13 12:16:34 1999 +0100
@@ -27,7 +27,7 @@
 
 (** Reflexivity **)
 
-Addsimps [order_refl];
+AddIffs [order_refl];
 
 (*This form is useful with the classical reasoner*)
 Goal "!!x::'a::order. x = y ==> x <= y";

--- a/src/HOL/UNITY/Network.ML	Wed Jan 13 12:08:51 1999 +0100
+++ b/src/HOL/UNITY/Network.ML	Wed Jan 13 12:16:34 1999 +0100
@@ -45,7 +45,7 @@
 by (dtac ([rs_AB, nondec_idle] MRS constrains_Int RS constrainsD) 1);
 by (assume_tac 1);
 by (ALLGOALS Asm_full_simp_tac);
-by (Blast_tac 1);
+by (blast_tac (claset() delrules [le0]) 1);
 by (Clarify_tac 1);
 by (subgoals_tac ["s' (Aproc, Rcvd) = s (Aproc, Rcvd)",
 		  "s' (Bproc, Rcvd) = s (Bproc, Rcvd)"] 1);