# HG changeset patch
# User nipkow
# Date 916226194 -3600
# Node ID c70bce7deb0f8d9c6900826a15c3655afbb2163b
# Parent  45958e54d72e8dc8f74f3a6da2090f74d09af699
Refined arithmetic.

diff -r 45958e54d72e -r c70bce7deb0f src/HOL/Arith.ML
--- 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!                             *)
diff -r 45958e54d72e -r c70bce7deb0f src/HOL/Integ/IntDef.ML
--- 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";
diff -r 45958e54d72e -r c70bce7deb0f src/HOL/Nat.ML
--- 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 _ => [
diff -r 45958e54d72e -r c70bce7deb0f src/HOL/NatDef.ML
--- 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]
diff -r 45958e54d72e -r c70bce7deb0f src/HOL/Ord.ML
--- 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";
diff -r 45958e54d72e -r c70bce7deb0f src/HOL/UNITY/Network.ML
--- 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);